equal
deleted
inserted
replaced
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 |