src/HOL/Library/Bit.thy
changeset 45701 615da8b8d758
parent 41959 b460124855b8
child 47108 2a1953f0d20d
--- a/src/HOL/Library/Bit.thy	Wed Nov 30 21:14:01 2011 +0100
+++ b/src/HOL/Library/Bit.thy	Wed Nov 30 23:30:08 2011 +0100
@@ -25,7 +25,7 @@
 
 end
 
-rep_datatype (bit) "0::bit" "1::bit"
+rep_datatype "0::bit" "1::bit"
 proof -
   fix P and x :: bit
   assume "P (0::bit)" and "P (1::bit)"