Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.2); Mon, 14 Dec 1992 02:35:44 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA06562; Sun, 13 Dec 92 18:16:41 -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 AA06552; Sun, 13 Dec 92 18:16:31 -0800 Received: from LocalHost.cs.ucla.edu by maui.cs.ucla.edu (Sendmail 5.61d+YP/3.21) id AA09056; Sun, 13 Dec 92 18:15:57 -0800 Message-Id: <9212140215.AA09056@maui.cs.ucla.edu> To: info-hol@edu.uidaho.cs.ted (INFO-HOL mailing list) Subject: Can't load library `more_lists` in draft mode Date: Sun, 13 Dec 92 18:15:56 PST From: chou@edu.ucla.cs Something's wrong with library `more_lists`: it can't be loaded in draft mode, as the following sessions show: [chou.38] hol =============================================================================== HOL88 Version 2.01 (NeXT/AKCL), built on 12/12/92 =============================================================================== #new_theory `foo` ;; () : void #load_library `more_lists` ;; Loading library more_lists ... .Loading library more_arithmetic ... Updating search path .Updating help search path .Declaring theory more_arithmetic a new parent Theory more_arithmetic loaded .......... Library more_arithmetic loaded. .Loading library auxiliary ... Updating search path .Declaring theory auxiliary a new parent Theory auxiliary loaded .................................................. Library auxiliary loaded. .Updating search path .Updating help search path .Declaring theory more_lists a new parent Theory more_lists loaded . unbound or non-assignable variable load_auxiliary 1 error in typing typecheck failed evaluation failed load -- /usr/local/src/hol/Library/more_lists/more_lists #quit();; Bye. [chou.39] hol =============================================================================== HOL88 Version 2.01 (NeXT/AKCL), built on 12/12/92 =============================================================================== #load_library `more_lists` ;; Loading library more_lists ... .Loading library more_arithmetic ... Updating search path .Updating help search path .Theory more_arithmetic loaded .......... Library more_arithmetic loaded. .Loading library auxiliary ... Updating search path .Defining ML function load_auxiliary ..... Library auxiliary loaded. .Updating search path .Updating help search path .Theory more_lists loaded .Loading contents of auxiliary... ............................................................ Library more_lists loaded. () : void #quit();; Bye. [chou.40]