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);
          Mon, 26 Oct 1992 13:54:41 +0000
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA28478;
          Mon, 26 Oct 92 03:45:21 -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 AA28473;
          Mon, 26 Oct 92 03:45:12 -0800
Received: from guillemot.cl.cam.ac.uk (user tfm) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.2) to cl; Mon, 26 Oct 1992 11:39:04 +0000
To: gavan@za.ac.uct.mth.elc (Gavan Tredoux)
Cc: info-hol@edu.uidaho.cs.ted, Tom.Melham@uk.ac.cam.cl
Subject: Re: prim_rec loading error?
In-Reply-To: Your message of Fri, 23 Oct 92 02:02:31 +0700. <9210230002.AA05419@elc.mth.uct.ac.za>
Date: Mon, 26 Oct 92 11:38:40 +0000
From: Tom Melham <Tom.Melham@uk.ac.cam.cl>
Message-Id: <"swan.cl.ca.943:26.09.92.11.39.12"@cl.cam.ac.uk>


> 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.

It is a deliberate policy (inasmuch as we actually have "policies")
to set up for autoloading only those theorems intended for general 
use, as opposed to theorems (and definitions) used only as intermediate
results in building a theory.  (There may also be erroneous ommissions).
Actually, such theorems really "shouldn't" be saved at all.

In this particular case, LESS_LEMMA2:

   |- !m n. (m = n) \/ (m < n) ==> m < SUC n

is used only in proving the stronger theorem LESS_THM:

   |- !m n. m < (SUC n)  =  (m  =  n)  \/  m < n

It is assumed that users will access the required fact through this
second theorem, so LESS_LEMMA2 is not set up to autoload.

Tom