Return-Path: Delivery-Date: Received: from dworshak.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Wed, 25 Aug 1993 08:27:53 +0100 Received: by dworshak.cs.uidaho.edu (1.37.109.4/16.2) id AA02198; Wed, 25 Aug 93 00:17:24 -0700 Sender: info-hol-request@cs.uidaho.edu Errors-To: info-hol-request@cs.uidaho.edu Precedence: bulk Received: from iraun1.ira.uka.de by dworshak.cs.uidaho.edu with SMTP (1.37.109.4/16.2) id AA02193; Wed, 25 Aug 93 00:17:20 -0700 Received: from ira.uka.de by iraun1.ira.uka.de with SMTP (PP) id <17700-0@iraun1.ira.uka.de>; Wed, 25 Aug 1993 09:08:08 +0200 Date: Wed, 25 Aug 93 9:10:23 MET DST From: reetz To: info-hol@dworshak.cs.uidaho.edu Subject: numerals by pretty printer instead by num_CONV? Message-Id: <"iraun1.ira.703:25.07.93.07.08.10"@ira.uka.de> Dear all, working with HOL90.5, I'm coming up here with just a little proposal: SUC(SUC(SUC...0) aren't fine to read, so there's num_CONV to provide natural number constants. But 1.) you have to use it by hand every time and 2.) it's done by mk_thm. So, why shouldn't the pretty printer print SUCs as natural number constants and leave the original term as it is? I myself don't have enough knowledge about the code of HOL90.5 to do the fix, but maybe anybody else cares or has already cared? (*****************************************************************************) (* *) (* Ralf Reetz SFB 358 of the german research society (DFG) *) (* reetz@ira.uka.de University of Karlsruhe, Germany *) (* *) (*****************************************************************************)