author | wenzelm |
Mon, 08 May 2000 20:59:30 +0200 | |
changeset 8840 | 18b76c137c41 |
parent 6988 | eed63543a3af |
child 9035 | 371f023d3dbd |
permissions | -rw-r--r-- |
(* Title: HOL/Numeral.thy ID: $Id$ Author: Larry Paulson and Markus Wenzel Generic numerals represented as twos-complement bitstrings. *) theory Numeral = Datatype files "Tools/numeral_syntax.ML":; datatype bin = Pls | Min | Bit bin bool (infixl "BIT" 90); axclass number < "term"; (*for numeric types: nat, int, real, ...*) consts number_of :: "bin => 'a::number"; syntax "_Numeral" :: "xnum => 'a" ("_"); setup NumeralSyntax.setup; end;