Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.4) outside ac.uk; Fri, 29 Jan 1993 07:54:13 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA17298; Thu, 28 Jan 93 23:35:45 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from Maui.CS.UCLA.EDU by ted.cs.uidaho.edu (16.6/1.34) id AA17293; Thu, 28 Jan 93 23:35:38 -0800 Received: from LocalHost.cs.ucla.edu by maui.cs.ucla.edu (Sendmail 5.61d+YP/3.21) id AA14949; Thu, 28 Jan 93 23:35:12 -0800 Message-Id: <9301290735.AA14949@maui.cs.ucla.edu> To: info-hol@edu.uidaho.cs.ted (INFO-HOL mailing list) Subject: Printing of assumptions Date: Thu, 28 Jan 93 23:35:11 PST From: chou@edu.ucla.cs With the subgoal package, is it possible to limit the printing of assumptions of a goal? I often have goals which have more than 40 assumptions. Not only it takes more time to print the goal than to execute the tactic, but the printed assumptions also fill the whole screen and I have to use the scroll bar to see the conclusion part of the goal. A good solution would be to print the first few items in the assumption list, where the new assumptions (resulting from, say, resolution tactics) appear. If I want to modify the code of the subgoal package, where is the code? And do I have to recompile HOL after the modification? If I recompile HOL, do I have to recompile my ML code and rebuild all the theories? - Ching Tsun