diff -r 9dcbf6a1829c -r 615da8b8d758 src/HOL/Library/Bit.thy --- 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)"