src/HOL/Numeral.thy
author oheimb
Wed Jan 31 10:15:55 2001 +0100 (2001-01-31)
changeset 11008 f7333f055ef6
parent 9410 612ee826a409
child 11488 4ff900551340
permissions -rw-r--r--
improved theory reference in comment
     1 (*  Title:      HOL/Numeral.thy
     2     ID:         $Id$
     3     Author:     Larry Paulson and Markus Wenzel
     4 
     5 Generic numerals represented as twos-complement bit strings.
     6 *)
     7 
     8 theory Numeral = Datatype
     9 files "Tools/numeral_syntax.ML":
    10 
    11 datatype
    12   bin = Pls
    13       | Min
    14       | Bit bin bool    (infixl "BIT" 90)
    15 
    16 axclass
    17   number < "term"      (*for numeric types: nat, int, real, ...*)
    18 
    19 consts
    20   number_of :: "bin => 'a::number"
    21 
    22 syntax
    23   "_Numeral" :: "xnum => 'a"    ("_")
    24 
    25 setup NumeralSyntax.setup
    26 
    27 end