Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Wed, 25 May 1994 06:51:57 +0100 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA10701; Tue, 24 May 1994 23:44:19 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: bulk Received: from irafs1.ira.uka.de by leopard.cs.byu.edu with SMTP (1.37.109.8/16.2) id AA10697; Tue, 24 May 1994 23:44:14 -0600 Received: from i80fs2.ira.uka.de (actually i80fs2) by irafs1 with SMTP (PP); Wed, 25 May 1994 07:39:59 +0200 Received: from ira.uka.de by i80fs2.ira.uka.de id <02808-0@i80fs2.ira.uka.de>; Wed, 25 May 1994 07:46:17 +0200 Date: Wed, 25 May 94 7:46:16 EDT From: reetz To: info-hol@leopard.cs.byu.edu, semaneth@cis.umassd.edu Subject: RE: cut elimination in HOL Message-Id: <"i80fs2.ira.810:25.04.94.05.46.20"@ira.uka.de> >My question is, how can I actually construct a proof tree that I can >thereafter manipulate. I'm not sure whether I got your problem right, but I think, you just looking for goal-directed proofs. These are possible in HOL. Look for set_goal, expand, top_thm, top_goal, backup, tactics,... hope this helps, Ralf val anonymous_hol_user_disclaimer = --`"if your only tool is a hammer, every problem looks like a nail!"`--; (* Ralf Reetz, reetz@ira.uka.de or reetz@informatik.uni-karlsruhe.de *)