equal
deleted
inserted
replaced
22 example and HOL/Library/Eval.thy for an ML example. |
22 example and HOL/Library/Eval.thy for an ML example. |
23 Superseedes some immature attempts. |
23 Superseedes some immature attempts. |
24 |
24 |
25 |
25 |
26 *** HOL *** |
26 *** HOL *** |
|
27 |
|
28 * Theorems "power.simps" renamed to "power_int.simps". |
27 |
29 |
28 * New class semiring_div provides basic abstract properties of semirings |
30 * New class semiring_div provides basic abstract properties of semirings |
29 with division and modulo operations. Subsumes former class dvd_mod. |
31 with division and modulo operations. Subsumes former class dvd_mod. |
30 |
32 |
31 * Merged theories IntDef, Numeral and IntArith into unified theory Int. |
33 * Merged theories IntDef, Numeral and IntArith into unified theory Int. |