src/HOL/Word/More_Word.thy
changeset 72292 4a58c38b85ff
parent 72262 a282abb07642
child 72388 633d14bd1e59
equal deleted inserted replaced
72291:ccc104786829 72292:4a58c38b85ff
    11   Bits_Int
    11   Bits_Int
    12   Misc_Auxiliary
    12   Misc_Auxiliary
    13   Misc_Arithmetic
    13   Misc_Arithmetic
    14   Misc_set_bit
    14   Misc_set_bit
    15   Misc_lsb
    15   Misc_lsb
       
    16   Misc_Typedef
    16 begin
    17 begin
    17 
    18 
    18 declare signed_take_bit_Suc [simp]
    19 declare signed_take_bit_Suc [simp]
    19 
    20 
    20 lemmas bshiftr1_def = bshiftr1_eq
    21 lemmas bshiftr1_def = bshiftr1_eq