src/HOL/Numeral.thy
author paulson
Thu Sep 23 13:06:31 1999 +0200 (1999-09-23)
changeset 7584 5be4bb8e4e3f
parent 6988 eed63543a3af
child 9035 371f023d3dbd
permissions -rw-r--r--
tidied; added lemma restrict_to_left
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;