equal
deleted
inserted
replaced
90 div_mult_mult1; theorems div_mult_mult1, div_mult_mult2, |
90 div_mult_mult1; theorems div_mult_mult1, div_mult_mult2, |
91 div_mult_mult1_if, div_mult_mult1 and div_mult_mult2 have been |
91 div_mult_mult1_if, div_mult_mult1 and div_mult_mult2 have been |
92 generalized to class semiring_div, subsuming former theorems |
92 generalized to class semiring_div, subsuming former theorems |
93 zdiv_zmult_zmult1, zdiv_zmult_zmult1_if, zdiv_zmult_zmult1 and |
93 zdiv_zmult_zmult1, zdiv_zmult_zmult1_if, zdiv_zmult_zmult1 and |
94 zdiv_zmult_zmult2. div_mult_mult1 is now [simp] by default. |
94 zdiv_zmult_zmult2. div_mult_mult1 is now [simp] by default. |
|
95 INCOMPATIBILITY. |
|
96 |
|
97 * Added theorem List.map_map as [simp]. Removed List.map_compose. |
95 INCOMPATIBILITY. |
98 INCOMPATIBILITY. |
96 |
99 |
97 * New testing tool "Mirabelle" for automated (proof) tools. Applies |
100 * New testing tool "Mirabelle" for automated (proof) tools. Applies |
98 several tools and tactics like sledgehammer, metis, or quickcheck, to |
101 several tools and tactics like sledgehammer, metis, or quickcheck, to |
99 every proof step in a theory. To be used in batch mode via the |
102 every proof step in a theory. To be used in batch mode via the |