src/HOL/Numeral.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Numeral.thy	Tue Jul 06 21:08:30 1999 +0200
@@ -0,0 +1,28 @@
+(*  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
+  numeral < "term";
+
+consts
+  number_of :: "bin => 'a::numeral";
+
+syntax
+  "_Numeral" :: "xnum => 'a"	("_");
+
+setup NumeralSyntax.setup;
+
+
+end;