Return-Path: <John.Harrison-request@cl.cam.ac.uk>
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, 19 Apr 1993 22:05:50 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA13733;
          Mon, 19 Apr 93 08:41:28 -0700
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Precedence: bulk
Received: from ULTRASTAR.EE.CORNELL.EDU by ted.cs.uidaho.edu (16.6/1.34) 
          id AA13728; Mon, 19 Apr 93 08:41:22 -0700
Date: Mon, 19 Apr 93 11:41:19 EDT
From: mel@ultrastar.EE.CORNELL.EDU (Miriam Leeser)
Received: by ultrastar.EE.CORNELL.EDU (4.1/1.6.10+n-y-Cornell-Electrical-Engineering) 
          id AA14464; Mon, 19 Apr 93 11:41:19 EDT
Message-Id: <9304191541.AA14464@ultrastar.EE.CORNELL.EDU>
To: info-hol@ted.cs.uidaho.edu
Subject: proof explanation mode


We are looking into a "proof explanation" mode in Nuprl, that is
different from the proof a user sees by applying tactics.  Are there
other proof systems that have feedback to the user distinct from the
level of interaction with the prover?