NEWS
changeset 32235 8f9b8d14fc9f
parent 32217 420108dd7dfe
child 32264 0be31453f698
equal deleted inserted replaced
32230:9f6461b1c9cc 32235:8f9b8d14fc9f
    64 
    64 
    65 * Power operations on relations and functions are now one dedicate
    65 * Power operations on relations and functions are now one dedicate
    66 constant compow with infix syntax "^^".  Power operations on
    66 constant compow with infix syntax "^^".  Power operations on
    67 multiplicative monoids retains syntax "^" and is now defined generic
    67 multiplicative monoids retains syntax "^" and is now defined generic
    68 in class power.  INCOMPATIBILITY.
    68 in class power.  INCOMPATIBILITY.
       
    69 
       
    70 * Relation composition "R O S" now has a "more standard" argument order,
       
    71 i.e., "R O S = {(x,z). EX y. (x,y) : R & (y,z) : S }".
       
    72 INCOMPATIBILITY: Rewrite propositions with "S O R" --> "R O S". Proofs
       
    73 may occationally break, since the O_assoc rule was not rewritten like this.
       
    74 Fix using O_assoc[symmetric].
       
    75 The same applies to the curried version "R OO S".
    69 
    76 
    70 * GCD now has functions Gcd/GCD and Lcm/LCM for the gcd and lcm of finite and
    77 * GCD now has functions Gcd/GCD and Lcm/LCM for the gcd and lcm of finite and
    71 infinite sets. It is shown that they form a complete lattice.
    78 infinite sets. It is shown that they form a complete lattice.
    72 
    79 
    73 * ML antiquotation @{code_datatype} inserts definition of a datatype
    80 * ML antiquotation @{code_datatype} inserts definition of a datatype