Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Wed, 19 May 1993 17:05:38 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA28735; Wed, 19 May 93 08:55:33 -0700 Sender: info-hol-request@ted.cs.uidaho.edu Errors-To: info-hol-request@ted.cs.uidaho.edu Precedence: bulk Received: from tuminfo2.informatik.tu-muenchen.de by ted.cs.uidaho.edu (16.6/1.34) id AA28730; Wed, 19 May 93 08:55:20 -0700 Received: from sunbroy14.informatik.tu-muenchen.de ([131.159.0.114]) by tuminfo2.informatik.tu-muenchen.de with SMTP id <57673>; Wed, 19 May 1993 17:55:16 +0200 Received: by sunbroy14.informatik.tu-muenchen.de id <8082>; Wed, 19 May 1993 17:54:35 +0200 From: Konrad Slind To: info-hol@ted.cs.uidaho.edu In-Reply-To: shb@oracorp.com's message of Wed, 19 May 1993 17:08:56 +0200 <9305191508.AA07266@sparta.oracorp.com> Subject: HOL90 style question Message-Id: <93May19.175435met_dst.8082@sunbroy14.informatik.tu-muenchen.de> Date: Wed, 19 May 1993 17:54:35 +0200 > Is there another technique for straightforwardly noting assumptions > about undefined functions without using axioms? You could use the abstract theory library to produce a "theory" parameterized by these assumptions. This package requires that you manage these assumptions/axioms yourself, although there is a rewriting structure and a goalstack modification in the library that take care of some of this for you. > If not, and if new_axiom really is the best tool for the job I used it > for, shouldn't HOL90 have its own version of new_axiom, without > requiring reference to HOL88? It does. Quoting from the online documentation for "new_axiom" in hol90: "hol90 doesn't have new_axiom; use new_open_axiom instead, which does not automatically generalize the term being asserted as an axiom." Konrad.