--- a/src/HOL/Numeral.thy Fri Aug 09 11:22:18 2002 +0200
+++ b/src/HOL/Numeral.thy Mon Aug 12 17:48:15 2002 +0200
@@ -8,6 +8,11 @@
theory Numeral = Datatype
files "Tools/numeral_syntax.ML":
+(* The constructors Pls/Min are hidden in numeral_syntax.ML.
+ Only qualified access bin.Pls/Min is allowed.
+ Should also hide Bit, but that means one cannot use BIT anymore.
+*)
+
datatype
bin = Pls
| Min
@@ -25,8 +30,8 @@
Numeral1 :: 'a
translations
- "Numeral0" == "number_of Pls"
- "Numeral1" == "number_of (Pls BIT True)"
+ "Numeral0" == "number_of bin.Pls"
+ "Numeral1" == "number_of (bin.Pls BIT True)"
setup NumeralSyntax.setup