Return-Path: <john.harrison-request@uk.ac.cam.cl>
Delivery-Date: 
Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.2);
          Fri, 23 Oct 1992 03:44:48 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA22604;
          Thu, 22 Oct 92 17:03:29 -0700
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Received: from Ucthpx.UCT.AC.ZA by ted.cs.uidaho.edu (16.6/1.34) id AA22598;
          Thu, 22 Oct 92 17:02:24 -0700
Received: by ucthpx.uct.ac.za (/\==/\ Smail3.1.24.1 #24.2) id m0miCQy-000NydC;
          Fri, 23 Oct 92 01:59 SAST
Received: by elc.mth.uct.ac.za (4.1/SMI-4.1) id AA05419;
          Fri, 23 Oct 92 02:02:33+020
From: gavan@za.ac.uct.mth.elc (Gavan Tredoux)
Message-Id: <9210230002.AA05419@elc.mth.uct.ac.za>
Subject: prim_rec loading error?
To: info-hol@edu.uidaho.cs.ted
Date: Fri, 23 Oct 92 2:02:31 EET
X-Mailer: ELM [version 2.3 PL11]

As I understand it, prim_rec is built-in and so all
theorems should be autoloaded. However LESS_LEMMA2,
which print_theory reveals as part of prim_rec,
doesn't load, it has to be explicitly loaded.

Anyone else have this problem?  Ok, it is a *small*
problem, but it's perplexing.

Gavan Tredoux
UCT