src/HOL/Library/Bit.thy
changeset 58306 117ba6cbe414
parent 55416 dd7992d4a61a
child 58881 b9556a055632
     1.1 --- a/src/HOL/Library/Bit.thy	Thu Sep 11 18:54:36 2014 +0200
     1.2 +++ b/src/HOL/Library/Bit.thy	Thu Sep 11 18:54:36 2014 +0200
     1.3 @@ -27,7 +27,7 @@
     1.4  
     1.5  end
     1.6  
     1.7 -rep_datatype "0::bit" "1::bit"
     1.8 +old_rep_datatype "0::bit" "1::bit"
     1.9  proof -
    1.10    fix P and x :: bit
    1.11    assume "P (0::bit)" and "P (1::bit)"