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"
     1 (*  Title:      HOL/Numeral.thy
     2     ID:         $Id$
     3     Author:     Larry Paulson and Markus Wenzel
     4 
     5 Generic numerals represented as twos-complement bitstrings.
     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 
    28 end;