equal
deleted
inserted
replaced
1 Isabelle NEWS -- history user-relevant changes |
1 Isabelle NEWS -- history user-relevant changes |
2 ============================================== |
2 ============================================== |
|
3 |
|
4 *** HOL *** |
|
5 |
|
6 * Class semiring_div now requires no_zero_divisors and proof of div_mult_mult1; |
|
7 theorems div_mult_mult1, div_mult_mult2, div_mult_mult1_if, div_mult_mult1 and |
|
8 div_mult_mult2 have been generalized to class semiring_div, subsuming former |
|
9 theorems zdiv_zmult_zmult1, zdiv_zmult_zmult1_if, zdiv_zmult_zmult1 and zdiv_zmult_zmult2. |
|
10 div_mult_mult1 is now [simp] by default. INCOMPATIBILITY. |
3 |
11 |
4 New in Isabelle2009 (April 2009) |
12 New in Isabelle2009 (April 2009) |
5 -------------------------------- |
13 -------------------------------- |
6 |
14 |
7 *** General *** |
15 *** General *** |