src/HOL/Integ/Bin.thy
changeset 6988 eed63543a3af
parent 6910 7c3503ae3d78
child 9207 0c294bd701ea
--- a/src/HOL/Integ/Bin.thy	Tue Jul 13 10:41:59 1999 +0200
+++ b/src/HOL/Integ/Bin.thy	Tue Jul 13 10:42:31 1999 +0200
@@ -40,7 +40,8 @@
   NCons_BIT "NCons (w BIT x) b = (w BIT x) BIT b"
 
 instance
-  int :: numeral 
+  int :: number
+
 primrec
   number_of_Pls  "number_of Pls = int 0"
   number_of_Min  "number_of Min = - (int 1)"