src/HOL/Numeral.thy
author nipkow
Mon, 29 Jan 2001 23:02:21 +0100
changeset 10996 74e970389def
parent 9410 612ee826a409
child 11488 4ff900551340
permissions -rw-r--r--
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy

(*  Title:      HOL/Numeral.thy
    ID:         $Id$
    Author:     Larry Paulson and Markus Wenzel

Generic numerals represented as twos-complement bit strings.
*)

theory Numeral = Datatype
files "Tools/numeral_syntax.ML":

datatype
  bin = Pls
      | Min
      | Bit bin bool    (infixl "BIT" 90)

axclass
  number < "term"      (*for numeric types: nat, int, real, ...*)

consts
  number_of :: "bin => 'a::number"

syntax
  "_Numeral" :: "xnum => 'a"    ("_")

setup NumeralSyntax.setup

end