Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Thu, 27 Oct 1994 02:04:13 +0000 Received: by leopard.cs.byu.edu (1.38.193.4/16.2) id AA20243; Wed, 26 Oct 1994 19:53:41 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: bulk Received: from csg.uwaterloo.ca by leopard.cs.byu.edu with SMTP (1.38.193.4/16.2) id AA20239; Wed, 26 Oct 1994 19:53:39 -0600 Received: by csg.uwaterloo.ca id <763>; Wed, 26 Oct 1994 21:47:48 -0400 Subject: problems with sem.ml in contrib/prog_logic92 From: Peter Bumbulis To: info-hol@leopard.cs.byu.edu Date: Wed, 26 Oct 1994 21:47:37 -0400 X-Mailer: ELM [version 2.3 PL11] Message-Id: <94Oct26.214748edt.763@csg.uwaterloo.ca> I'm having problems make'ing contrib/prog_logic92. Doing a "make clobber" followed by a "make all" stops with a lisp error in sem.ml: ... Theorem lub_first autoloading from theory `exseq` ... lub_first = |- !Ch. chain $<=| Ch ==> (first(lub $<=| Ch) = first(Ch 0)) Error: FUN%3009%1245 is invalid as a function. ... I've tried it wigh a couple of versions of HOL88/2.02 (Allegro/SunOS and gcl/Linux) with similar results (both versions of HOL have been rebuilt from scratch.) Any suggestions as to where I should start looking (the accompanying documentation suggests that it worked with HOL88/2.01.)? Thanks, Peter