equal
deleted
inserted
replaced
25 INCOMPATIBILITY. |
25 INCOMPATIBILITY. |
26 |
26 |
27 * New quickcheck implementation using new code generator. |
27 * New quickcheck implementation using new code generator. |
28 |
28 |
29 * New type class boolean_algebra. |
29 * New type class boolean_algebra. |
|
30 |
|
31 * Refinements to lattices classes: |
|
32 - added boolean_algebra type class |
|
33 - less default intro/elim rules in locale variant, more default |
|
34 intro/elim rules in class variant: more uniformity |
|
35 - lemma ge_sup_conv renamed to le_sup_iff, in accordance with le_inf_iff |
|
36 - dropped lemma alias inf_ACI for inf_aci (same for sup_ACI and sup_aci) |
|
37 - renamed ACI to inf_sup_aci |
30 |
38 |
31 * Class semiring_div requires superclass no_zero_divisors and proof of |
39 * Class semiring_div requires superclass no_zero_divisors and proof of |
32 div_mult_mult1; theorems div_mult_mult1, div_mult_mult2, |
40 div_mult_mult1; theorems div_mult_mult1, div_mult_mult2, |
33 div_mult_mult1_if, div_mult_mult1 and div_mult_mult2 have been |
41 div_mult_mult1_if, div_mult_mult1 and div_mult_mult2 have been |
34 generalized to class semiring_div, subsuming former theorems |
42 generalized to class semiring_div, subsuming former theorems |