NEWS
changeset 75085 ccc3a72210e6
parent 75081 d76b150efdc2
child 75087 f3fcc7c5a0db
equal deleted inserted replaced
75084:f700ca53e3ae 75085:ccc3a72210e6
    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 * Theory "HOL.Bit_Operations": rule bit_0 is not default [simp] any
       
    19 longer. INCOMPATIBILITY.
    17 
    20 
    18 * Theory "HOL.Relation": Added lemmas asymp_less and asymp_greater to
    21 * Theory "HOL.Relation": Added lemmas asymp_less and asymp_greater to
    19   type class preorder.
    22   type class preorder.
    20 
    23 
    21 * Theory "HOL-Library.Multiset":
    24 * Theory "HOL-Library.Multiset":