Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.2); Wed, 7 Oct 1992 21:36:44 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA04324; Wed, 7 Oct 92 13:19:42 -0700 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 AA04319; Wed, 7 Oct 92 13:19:35 -0700 Received: from LocalHost.cs.ucla.edu by maui.cs.ucla.edu (Sendmail 5.61d+YP/3.21) id AA25400; Wed, 7 Oct 92 13:18:42 -0700 Message-Id: <9210072018.AA25400@maui.cs.ucla.edu> To: info-hol@edu.uidaho.cs.ted Cc: chou@edu.ucla.cs Subject: My submissions to contrib Date: Wed, 07 Oct 92 13:18:41 PDT From: chou@edu.ucla.cs I have submitted three items to the "contrib" directory of HOL 2.1: (1) Definitions and theorems for generalizing any associative and commutative operation with identity to finite sets. (2) The ML code and documentation for the technique which I reported in "A Note on Interactive Theorem Proving with Theorem Continuation Functions" in the 1992 HOL Workshop. (3) A sequent formulation of a logic of predicates as reported in my other paper in the 1992 HOL Workshop. However, the codes have been improved so now the assumption list of a lifted sequent is a genuine list rather than the (lifted) conjunction of assumptions. If you are interested in obtaining a copy of any of the above before the release of HOL 2.1, please send me a message at . - Ching Tsun