Return-Path:
Return-Path: <john.harrison-request@uk.ac.cam.cl>
Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP) to cl
          id <22760-0@swan.cl.cam.ac.uk>; Fri, 1 Nov 1991 22:52:50 +0000
Received: by ted.cs.uidaho.edu (15.11/1.34) id AA10575;
          Fri, 1 Nov 91 10:56:53 pst
Reply-To: info-hol@ted
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@ted.cs.uidaho.edu
Received: from eros.uknet.ac.uk by ted.cs.uidaho.edu (15.11/1.34) id AA10571;
          Fri, 1 Nov 91 10:56:44 pst
X400-Received: by mta eros.uknet.ac.uk in /PRMD=UK.AC/ADMD=GOLD 400/C=GB/;
               Relayed; Fri, 1 Nov 1991 18:27:39 +0000
X400-Received: by /PRMD=icl/ADMD=gold 400/C=GB/; converted (ia5); Relayed;
               Fri, 1 Nov 1991 17:46:02 +0000
Date: Fri, 1 Nov 1991 17:46:02 +0000
X400-Originator: R.B.Jones@win0103.wins.icl.co.uk
X400-Mts-Identifier: [/PRMD=icl/ADMD=gold 400/C=GB/;win0103 0000020600000229]
Original-Encoded-Information-Types: undefined
X400-Content-Type: P2-1984 (2)
Content-Identifier: 229
From: R.B.Jones@win0103.wins.icl.co.uk
Message-Id: <"229*/I=RB/S=Jones/OU=win0103/O=icl/PRMD=icl/ADMD=gold 400/C=GB/"@MHS>
To: info-hol@edu.uidaho.cs.ted
Subject: assumptions and proof style







                            ASSUMPTIONS AND PROOF STYLE



         1.   Anyone who thinks the assumptions are a set shouldn't use
              FIRST_ASSUM.   Even ASM_REWRITE_TAC doesn't behave as if the
              assumptions are a set (and its not clear what it would mean
              for it to do so).

         2.   Anyone who expects non-trivial HOL proofs to be readable
              without seeing the output from HOL is likely to be
              dissappointed.

         3.   It is unrealistic to expect people to write proofs which will
              continue work when frequently used facilities like the
              resolution package change their behaviour.


         Roger Jones, International Computers Limited,

         R.B.Jones@win0103.uucp