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)"