Return-Path: <john.harrison-request@uk.ac.cam.cl>
Delivery-Date: 
Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.4) outside ac.uk; Mon, 29 Mar 1993 17:38:46 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA28934;
          Mon, 29 Mar 93 08:15:04 -0800
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Received: from netcom2.netcom.com by ted.cs.uidaho.edu (16.6/1.34) id AA28929;
          Mon, 29 Mar 93 08:14:57 -0800
Received: by netcom2.netcom.com (5.65/SMI-4.1/Netcom) id AA03539;
          Mon, 29 Mar 93 08:14:54 -0800
Date: Mon, 29 Mar 93 08:14:54 -0800
From: val@com.netcom (Dewey Val Schorre)
Message-Id: <9303291614.AA03539@netcom2.netcom.com>
To: info-hol@edu.uidaho.cs.ted
Subject: To: info-hol@ted.cs.uidaho.edu

Subject: Working with little memory

I don't have enough memory to load both the taut and arith library 
together, yet I need them for a proof. Is there a way to load the 
arith library, prove a theorem, save the proof on disk and load just 
the theorem or its proof without loading the whole arith library?

Val