Return-Path: <john.harrison-request@uk.ac.cam.cl>
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 03:54:39 +0000
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA05791;
          Sat, 16 Jan 93 19:43:27 -0800
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Received: from Maui.CS.UCLA.EDU by ted.cs.uidaho.edu (16.6/1.34) id AA05780;
          Sat, 16 Jan 93 19:43:16 -0800
Received: from LocalHost.cs.ucla.edu 
          by maui.cs.ucla.edu (Sendmail 5.61d+YP/3.21) id AA07386;
          Sat, 16 Jan 93 19:42:49 -0800
Message-Id: <9301170342.AA07386@maui.cs.ucla.edu>
To: info-hol@edu.uidaho.cs.ted (INFO-HOL mailing list)
Subject: New axiom with assumptions?
Date: Sat, 16 Jan 93 19:42:48 PST
From: chou@edu.ucla.cs

How can I postulate an axiom whose assumption list is not empty?
|new_axiom| doesn't allow me to do this.

My purpose is to use the axiom section of a theory file to
store those statements which I think is true but haven't yet
proved.  I need non-empty assumption lists in the axioms
because large portions of my theory is developed under a fixed
assumption, so it is convenient not to discharge that assumption
to the rhs of |- in the axioms and theorems.

- Ching Tsun