Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.2); Wed, 16 Dec 1992 16:12:27 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA17688; Wed, 16 Dec 92 07:50:15 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA17683; Wed, 16 Dec 92 07:50:00 -0800 Received: from coot.cl.cam.ac.uk (user pc) by swan.cl.cam.ac.uk with SMTP (PP-6.2) to cl; Wed, 16 Dec 1992 15:49:02 +0000 To: info-hol@edu.uidaho.cs.ted Cc: Paul.Curzon@uk.ac.cam.cl Subject: Re: Can't load library `more_lists` in draft mode Date: Wed, 16 Dec 92 15:48:45 +0000 From: Paul Curzon Message-Id: <"swan.cl.ca.591:16.11.92.15.49.05"@cl.cam.ac.uk> The files more_lists.ml and call_load_auxiliary.ml, which fix the bug in the loading of the library more_lists in HOL Version 2.01, are now available by ftp. They can be obtained by ftp from ftp.cl.cam.ac.uk in the directory hvg/contrib/more_lists_V21bugfix. They should be placed in the directory Library/more_lists/ In my last message: > The problem can also be avoided by loading the library before calling > new_parent. As Phil Windley pointed out, I did of course mean new_theory rather than new_parent. Paul.