NEWS
changeset 31547 398c0f48a99e
parent 31481 60ae1588f232
child 31626 fe35b72b9ef0
equal deleted inserted replaced
31546:d58d6acab331 31547:398c0f48a99e
     2 ==============================================
     2 ==============================================
     3 
     3 
     4 New in this Isabelle version
     4 New in this Isabelle version
     5 ----------------------------
     5 ----------------------------
     6 
     6 
       
     7 *** General ***
       
     8 
       
     9 * Discontinued old form of "escaped symbols" such as \\<forall>.  Only
       
    10 one backslash should be used, even in ML sources.
       
    11 
       
    12 
     7 *** Pure ***
    13 *** Pure ***
     8 
    14 
     9 * On instantiation of classes, remaining undefined class parameters are
    15 * On instantiation of classes, remaining undefined class parameters
    10 formally declared.  INCOMPATIBILITY.
    16 are formally declared.  INCOMPATIBILITY.
    11 
    17 
    12 
    18 
    13 *** HOL ***
    19 *** HOL ***
    14 
    20 
    15 * Class semiring_div requires superclass no_zero_divisors and proof of div_mult_mult1;
    21 * Class semiring_div requires superclass no_zero_divisors and proof of
    16 theorems div_mult_mult1, div_mult_mult2, div_mult_mult1_if, div_mult_mult1 and
    22 div_mult_mult1; theorems div_mult_mult1, div_mult_mult2,
    17 div_mult_mult2 have been generalized to class semiring_div, subsuming former
    23 div_mult_mult1_if, div_mult_mult1 and div_mult_mult2 have been
    18 theorems zdiv_zmult_zmult1, zdiv_zmult_zmult1_if, zdiv_zmult_zmult1 and zdiv_zmult_zmult2.
    24 generalized to class semiring_div, subsuming former theorems
    19 div_mult_mult1 is now [simp] by default.  INCOMPATIBILITY.
    25 zdiv_zmult_zmult1, zdiv_zmult_zmult1_if, zdiv_zmult_zmult1 and
    20 
    26 zdiv_zmult_zmult2.  div_mult_mult1 is now [simp] by default.
    21 * Power operations on relations and functions are now one dedicate constant compow with
    27 INCOMPATIBILITY.
    22 infix syntax "^^".  Power operations on multiplicative monoids retains syntax "^"
    28 
    23 and is now defined generic in class power.  INCOMPATIBILITY.
    29 * Power operations on relations and functions are now one dedicate
    24 
    30 constant compow with infix syntax "^^".  Power operations on
    25 * ML antiquotation @{code_datatype} inserts definition of a datatype generated
    31 multiplicative monoids retains syntax "^" and is now defined generic
    26 by the code generator; see Predicate.thy for an example.
    32 in class power.  INCOMPATIBILITY.
    27 
    33 
    28 * New method "linarith" invokes existing linear arithmetic decision procedure only.
    34 * ML antiquotation @{code_datatype} inserts definition of a datatype
       
    35 generated by the code generator; see Predicate.thy for an example.
       
    36 
       
    37 * New method "linarith" invokes existing linear arithmetic decision
       
    38 procedure only.
    29 
    39 
    30 
    40 
    31 *** ML ***
    41 *** ML ***
    32 
    42 
    33 * Eliminated old Attrib.add_attributes, Method.add_methods and related
    43 * Eliminated old Attrib.add_attributes, Method.add_methods and related