NEWS
changeset 75087 f3fcc7c5a0db
parent 75085 ccc3a72210e6
child 75091 445ec26fe47f
equal deleted inserted replaced
75086:4cc719621825 75087:f3fcc7c5a0db
    12 * Old-style {* verbatim *} tokens have been discontinued (legacy feature
    12 * Old-style {* verbatim *} tokens have been discontinued (legacy feature
    13 since Isabelle2019). INCOMPATIBILITY, use \<open>cartouche\<close> syntax instead.
    13 since Isabelle2019). INCOMPATIBILITY, use \<open>cartouche\<close> syntax instead.
    14 
    14 
    15 
    15 
    16 *** HOL ***
    16 *** HOL ***
       
    17 
       
    18 * Rule split_of_bool_asm is not split any longer, analogously to
       
    19 split_if_asm.  INCOMPATIBILITY.
    17 
    20 
    18 * Theory "HOL.Bit_Operations": rule bit_0 is not default [simp] any
    21 * Theory "HOL.Bit_Operations": rule bit_0 is not default [simp] any
    19 longer. INCOMPATIBILITY.
    22 longer. INCOMPATIBILITY.
    20 
    23 
    21 * Theory "HOL.Relation": Added lemmas asymp_less and asymp_greater to
    24 * Theory "HOL.Relation": Added lemmas asymp_less and asymp_greater to