equal
deleted
inserted
replaced
22 infix syntax "^^". Power operations on multiplicative monoids retains syntax "^" |
22 infix syntax "^^". Power operations on multiplicative monoids retains syntax "^" |
23 and is now defined generic in class power. INCOMPATIBILITY. |
23 and is now defined generic in class power. INCOMPATIBILITY. |
24 |
24 |
25 * ML antiquotation @{code_datatype} inserts definition of a datatype generated |
25 * ML antiquotation @{code_datatype} inserts definition of a datatype generated |
26 by the code generator; see Predicate.thy for an example. |
26 by the code generator; see Predicate.thy for an example. |
|
27 |
|
28 * New method "linarith" invokes existing linear arithmetic decision procedure only. |
27 |
29 |
28 |
30 |
29 *** ML *** |
31 *** ML *** |
30 |
32 |
31 * Eliminated old Attrib.add_attributes, Method.add_methods and related |
33 * Eliminated old Attrib.add_attributes, Method.add_methods and related |