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; Fri, 14 Jul 1995 16:30:26 +0100 Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA256474147; Fri, 14 Jul 1995 09:02:27 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: list Received: from crl.dec.com by leopard.cs.byu.edu with SMTP (1.37.109.15/16.2) id AA256414132; Fri, 14 Jul 1995 09:02:12 -0600 Received: by crl.dec.com; id AA04996; Fri, 14 Jul 95 10:57:34 -0400 Received: by easynet.crl.dec.com; id AA08351; Fri, 14 Jul 95 10:55:09 -0400 Message-Id: <9507141455.AA08351@easynet.crl.dec.com> Received: from ricks.enet; by crl.enet; Fri, 14 Jul 95 10:57:32 EDT Date: Fri, 14 Jul 95 10:57:32 EDT From: "Tim Leonard, DTN 225-5809, HLO2-3/C11" To: info-hol@leopard.cs.byu.edu Apparently-To: info-hol@leopard.cs.byu.edu Subject: Re: Easy theorem-provers -- not the Soft. Eng. answer I'm not calling for "dumming down" HOL either. When I suggest that the novice user should be able to use HOL knowing only a small number of comands, I was not intending to suggest that they necessarily be chosen from HOL's existing commands. If "grind" and a few others are a good set, the great thing about HOL is that they can be added. The question remains, What's a good set?