--- a/src/HOL/ex/BinEx.thy Thu Jul 08 13:46:29 1999 +0200
+++ b/src/HOL/ex/BinEx.thy Thu Jul 08 13:47:27 1999 +0200
@@ -9,7 +9,7 @@
Normal means no leading 0s on positive numbers and no leading 1s on negatives.
*)
-BinEx = Bin +
+BinEx = Main +
consts normal :: bin set