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; Thu, 26 Aug 1993 10:26:56 +0100 Received: by dworshak.cs.uidaho.edu (1.37.109.4/16.2) id AA03483; Thu, 26 Aug 93 02:23:56 -0700 Sender: info-hol-request@cs.uidaho.edu Errors-To: info-hol-request@cs.uidaho.edu Precedence: bulk Received: from swan.cl.cam.ac.uk by dworshak.cs.uidaho.edu with SMTP (1.37.109.4/16.2) id AA03479; Thu, 26 Aug 93 02:23:55 -0700 Received: from dunlin.cl.cam.ac.uk (user lcp (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Thu, 26 Aug 1993 10:23:50 +0100 To: info-hol@dworshak.cs.uidaho.edu Subject: numerals by pretty printer? Date: Thu, 26 Aug 93 10:23:45 +0100 From: Lawrence C Paulson Message-Id: <"swan.cl.cam.:074800:930826092353"@cl.cam.ac.uk> Isabelle does not, at present, support numerals. There is however an Isabelle theory of unlimited precision twos's complement binary integer arithmetic. Addition, subtraction and multiplication are performed by pure rewriting (Isabelle has no mk_thm). For example, evaluating 1359 * ~2468 = ~3354012 takes less than one minute on a Sun SS10. This theory resides on Isabelle's ZF set theory but could easily be transferred to Isabelle's HOL. Larry