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 <10629-0@swan.cl.cam.ac.uk>;
          Sat, 27 Apr 1991 21:02:28 +0100
Received: from vax.nsfnet-relay.ac.uk by sun2.nsfnet-relay.ac.uk
          with SMTP inbound id <13355-0@sun2.nsfnet-relay.ac.uk>;
          Sat, 27 Apr 1991 20:57:16 +0100
Received: from [129.101.100.20] by vax.NSFnet-Relay.AC.UK via NSFnet with SMTP
          id aa11917; 27 Apr 91 20:43 BST
Received: from sun2.nsfnet-relay.ac.uk by ted.cs.uidaho.edu (15.11/1.34)
          id AA16752; Sat, 27 Apr 91 12:49:48 pdt
Received: from computer-lab.cambridge.ac.uk by sun2.nsfnet-relay.ac.uk
          via JANET with NIFTP id <13199-0@sun2.nsfnet-relay.ac.uk>;
          Sat, 27 Apr 1991 20:47:09 +0100
Received: from guillemot.cl.cam.ac.uk by swan.cl.cam.ac.uk with SMTP (PP)
          id <10519-0@swan.cl.cam.ac.uk>; Sat, 27 Apr 1991 20:42:17 +0100
To: info-hol@edu.uidaho.cs.ted
Subject: saving theorems with hypotheses.
Date: Sat, 27 Apr 91 20:42:14 +0100
From: Tom.Melham@uk.ac.cam.cl
Message-Id: <"swan.cl.ca.521:27.03.91.19.42.20"@cl.cam.ac.uk>


For HOL version 13, I have restored the facility
to save theorems that have hypothses.

Tom