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
wenzelm@6905
     1
(*  Title:      HOL/Numeral.thy
wenzelm@6905
     2
    ID:         $Id$
wenzelm@6905
     3
    Author:     Larry Paulson and Markus Wenzel
wenzelm@6905
     4
wenzelm@9410
     5
Generic numerals represented as twos-complement bit strings.
wenzelm@6905
     6
*)
wenzelm@6905
     7
wenzelm@6905
     8
theory Numeral = Datatype
wenzelm@9035
     9
files "Tools/numeral_syntax.ML":
wenzelm@6905
    10
wenzelm@6905
    11
datatype
wenzelm@6905
    12
  bin = Pls
wenzelm@6905
    13
      | Min
wenzelm@9358
    14
      | Bit bin bool    (infixl "BIT" 90)
wenzelm@6905
    15
wenzelm@6905
    16
axclass
wenzelm@9035
    17
  number < "term"      (*for numeric types: nat, int, real, ...*)
wenzelm@6905
    18
wenzelm@6905
    19
consts
wenzelm@9035
    20
  number_of :: "bin => 'a::number"
wenzelm@6905
    21
wenzelm@6905
    22
syntax
wenzelm@9358
    23
  "_Numeral" :: "xnum => 'a"    ("_")
wenzelm@6905
    24
wenzelm@9035
    25
setup NumeralSyntax.setup
wenzelm@6905
    26
wenzelm@9035
    27
end