Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Thu, 23 Dec 1993 22:39:47 +0000
Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA02247;
          Thu, 23 Dec 1993 15:28:31 -0700
Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: bulk
Received: from dworshak.cs.uidaho.edu by leopard.cs.byu.edu 
          with SMTP (1.37.109.8/16.2) id AA02243;
          Thu, 23 Dec 1993 15:28:21 -0700
Received: from Maui.CS.UCLA.EDU by dworshak.cs.uidaho.edu 
          with SMTP (1.37.109.8/16.2) id AA21863;
          Thu, 23 Dec 1993 14:26:23 -0800
Received: from LocalHost.cs.ucla.edu 
          by maui.cs.ucla.edu (Sendmail 5.61d+YP/3.23) id AA19439;
          Thu, 23 Dec 93 14:26:10 -0800
Message-Id: <9312232226.AA19439@maui.cs.ucla.edu>
To: info-hol@cs.uidaho.edu
Subject: Re: Why can't theorems with assumptions be saved in a theory file?
Cc: slind@informatik.tu-muenchen.de
Date: Thu, 23 Dec 93 14:26:09 PST
From: chou@cs.ucla.edu

Several people pointed out to me that one can save theorems with assumptions
in theory files in HOL88.  However, one can't do so in HOL90.6, as the
following shows:

- new_theory "foo" ;

Declaring theory "foo".

Theory "HOL" already consistent with disk, hence not exported.
val it = () : unit

- save_thm ("abc", ASSUME (--`x=1`--))
= handle e => (print_HOL_ERR e ; ASSUME (--`x=1`--)) ;

Exception raised at Theory.save_thm:
non empty assumption set
val it = . |- x = 1 : thm

- print_theory "-" ;
Theory: foo

Parents:
    HOL

Type constants:
    


Term constants:
    


Axioms:
    


Definitions:
    


Theorems:
    


Theory "foo" is inconsistent with disk.
val it = () : unit


Perhaps this should be changed?

- Ching Tsun