--- a/src/HOL/Numeral.thy Sun Jun 04 00:09:04 2000 +0200
+++ b/src/HOL/Numeral.thy Sun Jun 04 19:39:29 2000 +0200
@@ -6,23 +6,23 @@
*)
theory Numeral = Datatype
-files "Tools/numeral_syntax.ML":;
+files "Tools/numeral_syntax.ML":
datatype
bin = Pls
| Min
- | Bit bin bool (infixl "BIT" 90);
+ | Bit bin bool (infixl "BIT" 90)
axclass
- number < "term"; (*for numeric types: nat, int, real, ...*)
+ number < "term" (*for numeric types: nat, int, real, ...*)
consts
- number_of :: "bin => 'a::number";
+ number_of :: "bin => 'a::number"
syntax
- "_Numeral" :: "xnum => 'a" ("_");
+ "_Numeral" :: "xnum => 'a" ("_")
-setup NumeralSyntax.setup;
+setup NumeralSyntax.setup
-end;
+end