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; Tue, 23 Aug 1994 17:28:31 +0100 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA26496; Tue, 23 Aug 1994 10:21:38 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: bulk Received: from babar.inria.fr by leopard.cs.byu.edu with SMTP (1.37.109.8/16.2) id AA26484; Tue, 23 Aug 1994 10:21:35 -0600 Received: by babar.inria.fr (5.65c8/IDA-1.2.8) id AA19332; Tue, 23 Aug 1994 18:18:57 +0200 Date: Tue, 23 Aug 1994 18:18:57 +0200 From: Laurent Thery Message-Id: <199408231618.AA19332@babar.inria.fr> To: info-hol@leopard.cs.byu.edu Subject: X interface for HOL Hi, my previous message apparently got lost. So I send it again. Apologies if you get multiple copies: I'm pleased to announce the first alpha release of the CHOL interface: ********************************************************************* What is CHOL? CHOL is an attempt to provide a better user-interface for the HOL theorem prover. It has been developed following a general approach for building user-interfaces for theorem provers. Its characteristics are the following: o graphic interface: multi fonts and colors are used to display formulas and proofs. o structured editing: The proof of a proposition is presented as the structured editing of the tactic that proves the proposition. o rewriting tool: A tool has been developed that filters the theorems of the database with respect to the term to rewrite. o separation between the interface and the prover: The X interface and HOL run as two separate processes. How to get it? For the mosaic addicts, there is a server: http://zenon.inria.fr:8003/croap/chol/chol.html For the others, a README and a tarfile are ftpable from: babar.inria.fr: /pub/centaur/chol Have fun, ************************************************************************* Laurent The'ry/ INRIA Sophia Antipolis / Laurent.Thery@inria.fr