equal
deleted
inserted
replaced
15 * On instantiation of classes, remaining undefined class parameters |
15 * On instantiation of classes, remaining undefined class parameters |
16 are formally declared. INCOMPATIBILITY. |
16 are formally declared. INCOMPATIBILITY. |
17 |
17 |
18 |
18 |
19 *** HOL *** |
19 *** HOL *** |
|
20 |
|
21 * Refinements to lattices classes: |
|
22 - added boolean_algebra type class |
|
23 - less default intro/elim rules in locale variant, more default |
|
24 intro/elim rules in class variant: more uniformity |
|
25 - lemma ge_sup_conv renamed to le_sup_iff, in accordance with le_inf_iff |
|
26 - dropped lemma alias inf_ACI for inf_aci (same for sup_ACI and sup_aci) |
|
27 - renamed ACI to inf_sup_aci |
20 |
28 |
21 * Class semiring_div requires superclass no_zero_divisors and proof of |
29 * Class semiring_div requires superclass no_zero_divisors and proof of |
22 div_mult_mult1; theorems div_mult_mult1, div_mult_mult2, |
30 div_mult_mult1; theorems div_mult_mult1, div_mult_mult2, |
23 div_mult_mult1_if, div_mult_mult1 and div_mult_mult2 have been |
31 div_mult_mult1_if, div_mult_mult1 and div_mult_mult2 have been |
24 generalized to class semiring_div, subsuming former theorems |
32 generalized to class semiring_div, subsuming former theorems |