src/HOL/Library/Bit.thy
changeset 58306 117ba6cbe414
parent 55416 dd7992d4a61a
child 58881 b9556a055632
equal deleted inserted replaced
58305:57752a91eec4 58306:117ba6cbe414
    25 
    25 
    26 instance ..
    26 instance ..
    27 
    27 
    28 end
    28 end
    29 
    29 
    30 rep_datatype "0::bit" "1::bit"
    30 old_rep_datatype "0::bit" "1::bit"
    31 proof -
    31 proof -
    32   fix P and x :: bit
    32   fix P and x :: bit
    33   assume "P (0::bit)" and "P (1::bit)"
    33   assume "P (0::bit)" and "P (1::bit)"
    34   then have "\<forall>b. P (Bit b)"
    34   then have "\<forall>b. P (Bit b)"
    35     unfolding zero_bit_def one_bit_def
    35     unfolding zero_bit_def one_bit_def