Return-Path:
Return-Path: <john.harrison-request@uk.ac.cam.cl>
Received: from nsf.ac.uk by swan.cl.cam.ac.uk via JANET
          with NIFTP to fgate (PP) id <5034-0@swan.cl.cam.ac.uk>;
          Thu, 4 Apr 1991 14:50:41 +0100
Received: from vax.nsfnet-relay.ac.uk by sun2.nsfnet-relay.ac.uk
          with SMTP inbound id <7676-0@sun2.nsfnet-relay.ac.uk>;
          Thu, 4 Apr 1991 11:26:25 +0100
Received: from [129.101.100.20] by vax.NSFnet-Relay.AC.UK via NSFnet with SMTP
          id aa04283; 4 Apr 91 11:29 BST
Received: from sun2.nsfnet-relay.ac.uk by ted.cs.uidaho.edu (15.11/1.34)
          id AA17605; Thu, 4 Apr 91 02:16:26 pst
Received: from computer-lab.cambridge.ac.uk by sun2.nsfnet-relay.ac.uk
          via JANET with NIFTP id <6712-0@sun2.nsfnet-relay.ac.uk>;
          Thu, 4 Apr 1991 10:43:32 +0100
Received: from coot.cl.cam.ac.uk by swan.cl.cam.ac.uk with SMTP (PP)
          id <27103-0@swan.cl.cam.ac.uk>; Thu, 4 Apr 1991 10:45:23 +0100
To: info-hol@edu.uidaho.cs.ted
Subject: Theories of Lists
Date: Thu, 04 Apr 91 10:45:26 +0100
From: Paul.Curzon@uk.ac.cam.cl
Message-Id: <"swan.cl.ca.108:04.03.91.09.45.27"@cl.cam.ac.uk>


Hi folks,

Has anyone extended the HOL theory of lists? In particular I
currently need definitions and theorems concerning the subtraction
of lists from the front of other lists and tests for lists being
initial sublists of other lists.  Any other general theorems or
definitions might also be useful.

Thanks
        Paul Curzon.