Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.4); Mon, 4 Jan 1993 15:23:15 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA20485; Mon, 4 Jan 93 07:13:37 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from Ucthpx.UCT.AC.ZA by ted.cs.uidaho.edu (16.6/1.34) id AA20480; Mon, 4 Jan 93 07:13:27 -0800 Received: by ucthpx.uct.ac.za (/\==/\ Smail3.1.24.1 #24.2) id m0n8tTS-000NyvC; Mon, 4 Jan 93 17:12 SAST Received: by elc.mth.uct.ac.za (4.1/SMI-4.1) id AA09726; Mon, 4 Jan 93 17:12:59+020 From: gavan@za.ac.uct.mth.elc (Gavan Tredoux) Message-Id: <9301041512.AA09726@elc.mth.uct.ac.za> Subject: latex-hol problem To: info-hol@edu.uidaho.cs.ted Date: Mon, 4 Jan 93 17:12:55 EET X-Mailer: ELM [version 2.3 PL11] I've just tried to use the latex-hol library packaged with HOL 2.01, and after loading the library nothing seems to work anymore, as the following transcript shows ------------------------------begin transcript--------------------------------- =============================================================================== HOL88 Version 2.01 (SUN4/AKCL), built on 10/12/92 =============================================================================== ..............................................................() : void .................................................................() : void ..................() : void File hol-init loaded () : void #new_theory `foo`;; () : void #INDUCTION;; Theorem INDUCTION autoloading from theory `num` ... INDUCTION = |- !P. P 0 /\ (!n. P n ==> P(SUC n)) ==> (!n. P n) |- !P. P 0 /\ (!n. P n ==> P(SUC n)) ==> (!n. P n) #load_library `latex-hol`;; Loading library latex-hol ... Updating search path . Updating help search path .Loading library prettyp ... Updating help search path .................................................................................................................................................................................................................................................................................................... Library prettyp loaded. .................................................. Library latex-hol loaded. () : void #INDUCTION;; Error: The tag EVALUATION is undefined. Fast links are on: do (use-fast-links nil) for debugging Error signalled by TML. Error: 4 is an illegal ihs index. Fast links are on: do (use-fast-links nil) for debugging Error signalled by SYSTEM:UNIVERSAL-ERROR-HANDLER. Backtrace: SYSTEM:UNIVERSAL-ERROR-HANDLER Error: The tag (NIL) is undefined. Fast links are on: do (use-fast-links nil) for debugging Error signalled by SYSTEM:UNIVERSAL-ERROR-HANDLER. Backtrace: SYSTEM:UNIVERSAL-ERROR-HANDLER Error: The tag (NIL) is undefined. Fast links are on: do (use-fast-links nil) for debugging Error signalled by SYSTEM:UNIVERSAL-ERROR-HANDLER. Backtrace: SYSTEM:UNIVERSAL-ERROR-HANDLER --------------------------------end transcript--------------------------------- The last message repeats until the core dumps. This was run on a SPARC elc, using as the banner shows, AKCL common lisp. Ver 2.01 seems OK running other things. Gavan Tredoux FACCS Lab Dept Math UCT