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; Thu, 13 Jul 1995 17:20:51 +0100 Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA177220295; Thu, 13 Jul 1995 09:44:55 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: list Received: from swan.cl.cam.ac.uk by leopard.cs.byu.edu with ESMTP (1.37.109.15/16.2) id AA176469977; Thu, 13 Jul 1995 09:39:37 -0600 Received: from albatross.cl.cam.ac.uk (user sk (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Thu, 13 Jul 1995 16:40:22 +0100 To: info-hol@leopard.cs.byu.edu, Holger Busch Subject: Re: Conditionals In-Reply-To: Your message of "Thu, 13 Jul 1995 09:31:21 +0200." <199507130731.AA12865@borel.zfe.siemens.de> Date: Thu, 13 Jul 1995 16:40:09 +0100 From: Sara Kalvala Message-Id: <"swan.cl.cam.:087450:950713154027"@cl.cam.ac.uk> > accessible. To me there does not appear to be a contradiction between > offering powerful and easy-to-use "catch all tactics" and keeping the > architecture of HOL or LAMBDA open. I agree with this, specially if the tools are general and non-trivial. On the other hand, i've seen several cases where many functions that *could* be written in one line by users are made part of the core, which makes the core large and bulky and moreover make it very hard for people to know what really is the core. And I think one neat thing about LCF systems is that it is possible to separate the core of the prover from bells-and-whistles. Maybe the solution is to have a newbie library, where users get all sorts of short cuts to make it easy to do proofs to begin with, but which is well doumented and which new users should examine when they graduate to intermediate level. - Sara