src/HOL/Numeral.thy
author paulson
Tue Jul 13 10:42:31 1999 +0200 (1999-07-13)
changeset 6988 eed63543a3af
parent 6905 9bc05ec3497b
child 9035 371f023d3dbd
permissions -rw-r--r--
renamed sort "numeral" to "number"
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@6905
     5
Generic numerals represented as twos-complement bitstrings.
wenzelm@6905
     6
*)
wenzelm@6905
     7
wenzelm@6905
     8
theory Numeral = Datatype
wenzelm@6905
     9
files "Tools/numeral_syntax.ML":;
wenzelm@6905
    10
wenzelm@6905
    11
datatype
wenzelm@6905
    12
  bin = Pls
wenzelm@6905
    13
      | Min
wenzelm@6905
    14
      | Bit bin bool	(infixl "BIT" 90);
wenzelm@6905
    15
wenzelm@6905
    16
axclass
paulson@6988
    17
  number < "term";      (*for numeric types: nat, int, real, ...*)
wenzelm@6905
    18
wenzelm@6905
    19
consts
paulson@6988
    20
  number_of :: "bin => 'a::number";
wenzelm@6905
    21
wenzelm@6905
    22
syntax
wenzelm@6905
    23
  "_Numeral" :: "xnum => 'a"	("_");
wenzelm@6905
    24
wenzelm@6905
    25
setup NumeralSyntax.setup;
wenzelm@6905
    26
wenzelm@6905
    27
wenzelm@6905
    28
end;