Return-Path: Return-Path: Received: from nsf.ac.uk by swan.cl.cam.ac.uk via JANET with NIFTP to fgate (PP) id <27716-0@swan.cl.cam.ac.uk>; Fri, 26 Apr 1991 02:10:46 +0100 Received: from vax.nsfnet-relay.ac.uk by sun2.nsfnet-relay.ac.uk with SMTP inbound id <2230-12@sun2.nsfnet-relay.ac.uk>; Fri, 26 Apr 1991 02:06:22 +0100 Received: from [129.101.100.20] by vax.NSFnet-Relay.AC.UK via NSFnet with SMTP id aa27089; 26 Apr 91 1:54 BST Received: from panther.cs.uidaho.edu by ted.cs.uidaho.edu (15.11/1.34) id AA08700; Thu, 25 Apr 91 17:56:53 pdt Received: by panther.cs.uidaho.edu (5.57/Ultrix3.0-C) id AA14977; Thu, 25 Apr 91 17:59:03 -0700 Message-Id: <9104260059.AA14977@panther.cs.uidaho.edu> To: info-hol@edu.uidaho.cs.ted Subject: save_thm and hypostheses/ abstract theories Date: Thu, 25 Apr 91 17:59:02 PDT From: Phil Windley HOL 1.12 will not save theorems with hypotheses. The function save_thm fails with an appropriate error message. HOL 1.11 did allow this and I rely on it. Why was this changed? Is there a security problem or just a technical one? I'd like to be able to save theorems with hypostheses if it is not a security concern. On a related note: At HOL89 Elsa Gunter talked about abstract theories. Is anyone working on these? I was thinking about devoting some time to this if no one else was. The reason that I rely on theorems with hypotheses is that I fake abstract theories using them. I wouldn't care if I had true abstract theories (although if HOL is to be sequent based, theorems with hypotheses seem like a reasonable thing to allow). --phil--