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; Tue, 11 Jan 1994 16:42:20 +0000 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA14141; Tue, 11 Jan 1994 09:34:14 -0700 Sender: info-hol-request@leopard.cs.byu.edu Errors-To: info-hol-request@leopard.cs.byu.edu Precedence: bulk Received: from dworshak.cs.uidaho.edu by leopard.cs.byu.edu with SMTP (1.37.109.8/16.2) id AA14136; Tue, 11 Jan 1994 09:33:58 -0700 Received: from iraun1.ira.uka.de by dworshak.cs.uidaho.edu with SMTP (1.37.109.8/16.2) id AA13985; Tue, 11 Jan 1994 08:31:49 -0800 Received: from ira.uka.de by iraun1.ira.uka.de id <01588-0@iraun1.ira.uka.de>; Tue, 11 Jan 1994 17:05:03 +0100 Received: from ira.uka.de by i80fs2.ira.uka.de id <01023-0@i80fs2.ira.uka.de>; Tue, 11 Jan 1994 17:05:44 +0100 Date: Tue, 11 Jan 94 17:05:43 EST From: reetz To: kevin@dcs.ed.ac.uk Cc: info-hol@cs.uidaho.edu Subject: RE: A problem building Hol90.6 Message-Id: <"i80fs2.ira.025:11.00.94.16.06.01"@ira.uka.de> Kevin has had a problem with theories in HOL90.6 with appears only once and then, it looks like it works. Changing to HOL90.6, I've had the same effect with other theories. After building ALL theories anew and using load_library for theories like string instead, the problem disappeared. This isn't an explanation, but it has helped. :) Ralf (*****************************************************************************) (* *) (* Ralf Reetz SFB 358 of the german research *) (* reetz@informatik.uni-karlsruhe.de society (DFG) *) (* University of Karlsruhe, Germany *) (* *) (* "we prove around in a ring and suppose, *) (* the goal sits right in the middle and knows." *) (* *) (*****************************************************************************)