author | wenzelm |
Mon, 12 Jul 1999 22:27:20 +0200 | |
changeset 6981 | eaade7e398a7 |
parent 6905 | 9bc05ec3497b |
child 6988 | eed63543a3af |
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 numeral < "term"; consts number_of :: "bin => 'a::numeral"; syntax "_Numeral" :: "xnum => 'a" ("_"); setup NumeralSyntax.setup; end;