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, 24 May 1994 08:22:45 +0100 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA00406; Tue, 24 May 1994 01:21:36 -0600 Sender: hol2000-request@lal.cs.byu.edu Errors-To: hol2000-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 AA00402; Tue, 24 May 1994 01:21:30 -0600 Received: from i80fs2.ira.uka.de (actually i80fs2) by irafs1 with SMTP (PP); Tue, 24 May 1994 09:07:08 +0200 Received: from ira.uka.de by i80fs2.ira.uka.de id <28730-0@i80fs2.ira.uka.de>; Tue, 24 May 1994 09:13:25 +0200 Date: Tue, 24 May 94 9:13:24 EDT From: reetz To: hol2000@leopard.cs.byu.edu Subject: RE: hol2000 is very silent Message-Id: <"i80fs2.ira.732:24.04.94.07.13.27"@ira.uka.de> I myself switched from hol88 to hol90 with a LOT of work. Everything from programs, proofs, lectures for students to documentation had to be changed. IMHO is was worth, but it shows a problem with hol2000: I myself am not very encouraged to switch to another new hol again. Instead, I am looking forward to improvements of hol90! I'm just interested what's going on there with other hol-versions. Maybe my personal view is one reason for the hol2000 mailing list being silent. Maybe other people around might like to discuss that point... (*****************************************************************************) (* *) (* Ralf Reetz SFB 358 of the german research *) (* reetz@informatik.uni-karlsruhe.de society (DFG) *) (* reetz@ira.uka.de University of Karlsruhe, Germany *) (* *) (* "we prove around in a ring and suppose, *) (* the goal sits right in the middle and knows." *) (* *) (*****************************************************************************)