Return-Path: Delivery-Date: Received: from dworshak.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Wed, 1 Sep 1993 21:51:09 +0100 Received: by dworshak.cs.uidaho.edu (1.37.109.4/16.2) id AA13466; Wed, 1 Sep 93 13:45:11 -0700 Sender: info-hol-request@cs.uidaho.edu Errors-To: info-hol-request@cs.uidaho.edu Precedence: bulk Received: from swan.cl.cam.ac.uk by dworshak.cs.uidaho.edu with SMTP (1.37.109.4/16.2) id AA13458; Wed, 1 Sep 93 13:44:51 -0700 Received: from albatross.cl.cam.ac.uk (user sk (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Wed, 1 Sep 1993 21:44:45 +0100 To: chou@cs.ucla.edu Cc: info-hol@dworshak.cs.uidaho.edu Subject: Re: HOL improvement survey In-Reply-To: Your message of "Wed, 25 Aug 93 22:13:50 PDT." <9308260513.AA11253@maui.cs.ucla.edu> Date: Wed, 01 Sep 93 21:44:41 +0100 From: Sara Kalvala Message-Id: <"swan.cl.cam.:050880:930901204448"@cl.cam.ac.uk> From: chou@cs.ucla.edu > How to make HOL proofs more readable and closer to the ordinary > "textbook style" presentation? While proofs themselves *can* be made to be more readable (either by using a readable language of (say) tactics or by a good mix of forward and backward proof), I still think that one needs good commentary to make proofs understandable. In my paper for the Leuven HOL meeting (1992) I have described a way to do this using annotations. My implementation, however, doesn't work with the new release of HOL90 due to the change to representation of terms; a changed version of the annotation stuff will be available "soon". - Sara