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; Fri, 24 Dec 1993 11:02:02 +0000
Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA04943;
          Fri, 24 Dec 1993 03:45:51 -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 AA04939;
          Fri, 24 Dec 1993 03:45:31 -0700
Received: from iraun1.ira.uka.de by dworshak.cs.uidaho.edu 
          with SMTP (1.37.109.8/16.2) id AA23251;
          Fri, 24 Dec 1993 02:43:36 -0800
Received: from ira.uka.de by iraun1.ira.uka.de id <28372-0@iraun1.ira.uka.de>;
          Fri, 24 Dec 1993 11:43:31 +0100
Received: from ira.uka.de by i80fs2.ira.uka.de id <07938-0@i80fs2.ira.uka.de>;
          Fri, 24 Dec 1993 11:44:25 +0100
Date: Fri, 24 Dec 93 11:44:24 EST
From: reetz <reetz@ira.uka.de>
To: info-hol@cs.uidaho.edu
Cc: chou@cs.ucla.edu
Subject: RE: theorems can have assumptions in hol90.6
Message-Id: <"i80fs2.ira.940:24.11.93.10.44.30"@ira.uka.de>

Ching Tsun has asked, whether hol90.6 can have assumptions
in stored theorems. It is possible. You have to set a flag:

allow_theorems_with_assumptions := true;
val it = () : unit
- new_theory "foo";
save_thm("heinz",ASSUME (--`T`--));
val it = [T] |- T : thm
- print_theory "-";
Theory: foo
 
Parents:
    CSM_deltadelay
 
Type constants:
    
 
Term constants:
    
 
Axioms:
    
 
Definitions:
    
 
Theorems:
    heinz [T] |- T
 
Theory "foo" is inconsistent with disk.
val it = () : unit


merry christmas and happy new year!  :) Ralf

                                &&&&&&&&&&&&
                              &&&&&&&&&&&&&&&&
                             &&&&&        &&&&&
                            &&&&&          &&&&&
                            &&&&____ __ ____&&&&
                             &&|   _|__|_   |&&
                              &&---/ /\ \---&&
                                &&| |&&| |&& 
                                  |_|  |_|   


(*****************************************************************************)
(*                                                                           *)
(*  Ralf Reetz                 SFB 358 of the german research society (DFG)  *)
(*  reetz@ira.uka.de           University of Karlsruhe, Germany              *)
(*                                                                           *)
(*                "we prove around in a ring and suppose,                    *)
(*                 the goal sits right in the middle and knows."             *)
(*                                                                           *)
(*****************************************************************************)