Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.4); Sun, 17 Jan 1993 08:51:43 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA06924; Sun, 17 Jan 93 00:44:38 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA06919; Sun, 17 Jan 93 00:44:32 -0800 Received: from albatross.cl.cam.ac.uk (user mjcg (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.4) to cl; Sun, 17 Jan 1993 08:44:01 +0000 Received: by albatross.cl.cam.ac.uk (4.1/SMI-3.0DEV3) id AA18443; Sun, 17 Jan 93 08:43:57 GMT Date: Sun, 17 Jan 93 08:43:57 GMT From: Mike.Gordon@uk.ac.cam.cl Message-Id: <9301170843.AA18443@albatross.cl.cam.ac.uk> To: chou@edu.ucla.cs Cc: info-hol@edu.uidaho.cs.ted In-Reply-To: chou@edu.ucla.cs's message of Sat, 16 Jan 93 19:42:48 PST <9301170342.AA07386@maui.cs.ucla.edu> Subject: New axiom with assumptions? Regarding axioms with assumptions: ---------------------------------- In the theory `bool` there is an infixed constant IS_ASSUMPTION_OF defined by: |- !t1 t2. t1 IS_ASSUMPTION_OF t2 = t1 ==> t2 This is used by the implementation of theories to encode theorems with assumptions as theorems without assumptions (see ml/hol-thyfn.ml). I think you could use this constant to implement functions: new_asm_axiom asm_axiom that stored and retrieved axioms with assumptions as axioms without them. Admittedly a hack .. but at least a logically kosher one! Regarding the dropping of assumptions by tactics: ------------------------------------------------- Historical note: this behaviour is part of the concept of tactics as originally invented by Robin Milner. See early LCF writings on the notion of "achievement". Perhaps it is more appropriate for LCF than for HOL? Mike