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, 26 May 1994 17:00:06 +0100 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA24774; Thu, 26 May 1994 08:50:16 -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 AA24770; Thu, 26 May 1994 08:50:11 -0600 Received: from i80fs2.ira.uka.de (actually i80fs2) by irafs1 with SMTP (PP); Thu, 26 May 1994 16:45:50 +0200 Received: from ira.uka.de by i80fs2.ira.uka.de id <09797-0@i80fs2.ira.uka.de>; Thu, 26 May 1994 16:52:14 +0200 Date: Thu, 26 May 94 16:52:12 EDT From: reetz To: hol2000@leopard.cs.byu.edu Subject: rewrite as primitive? Message-Id: <"i80fs2.ira.799:26.04.94.14.52.17"@ira.uka.de> Considering whether rewrite should be or should not be made a primitive in hol2000, I would like to suggest the following: the user might like to choose between "fast" and "secure" proofs. There might be even different levels between "very fast" and "very secure". In fact, that should be translated into: "use as much as it speeds things up as primitive" versus "use as less as possible as primitives". Or: "use a hol proof" versus "use a bdd-package". This might be realised by a general flag, which is read by the conversions, which should then decide itselfs, what proof methods it wants to use. Ralf. val anonymous_hol_user_disclaimer = --`"if your only tool is a hammer, every problem looks like a nail!"`--; (* Ralf Reetz, reetz@ira.uka.de or reetz@informatik.uni-karlsruhe.de *)