equal
deleted
inserted
replaced
6 * Class semiring_div now requires no_zero_divisors and proof of div_mult_mult1; |
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 |
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 |
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. |
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. |
10 div_mult_mult1 is now [simp] by default. INCOMPATIBILITY. |
|
11 |
|
12 * Power operation on relations and functions is now a dedicated overloaded constant |
|
13 funpower with infix syntax "^^". INCOMPATIBILITY. |
11 |
14 |
12 New in Isabelle2009 (April 2009) |
15 New in Isabelle2009 (April 2009) |
13 -------------------------------- |
16 -------------------------------- |
14 |
17 |
15 *** General *** |
18 *** General *** |