Return-Path: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) id <27719-0@swan.cl.cam.ac.uk>; Thu, 18 Jun 1992 16:02:06 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA05708; Thu, 18 Jun 92 07:48:11 -0700 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Received: from infix.cs.ruu.nl by ted.cs.uidaho.edu (16.6/1.34) id AA05703; Thu, 18 Jun 92 07:47:56 -0700 Received: by infix.cs.ruu.nl id AA15115 (5.65c/IDA-1.4.4 for info-hol@ted.cs.uidaho.edu); Thu, 18 Jun 1992 16:48:42 +0200 From: Wishnu Prasetya Message-Id: <199206181448.AA15115@infix.cs.ruu.nl> Subject: Failure to load Abstract Theory To: info-hol@edu.uidaho.cs.ted (hol mailing list) Date: Thu, 18 Jun 92 16:48:40 METDST X-Mailer: ELM [version 2.3 PL11] > A new version of the abstract theory package is available for anonymous FTP > from cs.uidaho.edu. > > The new version of the Abstract Theory package provides the following > features not found in the original: > > o Abstract representations create a real type that can be used to > conveniently form expressions. > > o The process of creating abstract representations has been speeded up > substantially. There is no longer the need to have special functions for > accessing the abstract type or creating the instantiation theorems. > I tried to load `abs_theory`, but fail with the following report: unbound or non-assignable variable abs_theory 2 errors in typing Anyone have any idea why? Or perhaps HOL 2.0 is required for the package? Thanks. -Wishnu Prasetya- --