src/HOL/Numeral.thy
author berghofe
Tue, 30 May 2000 18:02:49 +0200
changeset 9001 93af64f54bf2
parent 6988 eed63543a3af
child 9035 371f023d3dbd
permissions -rw-r--r--
the is now defined using primrec, avoiding explicit use of arbitrary.

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

Generic numerals represented as twos-complement bitstrings.
*)

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;