equal
deleted
inserted
replaced
32 HOL/Library/Eval.thy for an ML example. Supersedes previous |
32 HOL/Library/Eval.thy for an ML example. Supersedes previous |
33 experimental versions. |
33 experimental versions. |
34 |
34 |
35 |
35 |
36 *** HOL *** |
36 *** HOL *** |
|
37 |
|
38 * Theorem Inductive.lfp_ordinal_induct generalized to complete lattices. The |
|
39 form set-specific version is available as Inductive.lfp_ordinal_induct_set. |
37 |
40 |
38 * Theorems "power.simps" renamed to "power_int.simps". |
41 * Theorems "power.simps" renamed to "power_int.simps". |
39 |
42 |
40 * New class semiring_div provides basic abstract properties of semirings |
43 * New class semiring_div provides basic abstract properties of semirings |
41 with division and modulo operations. Subsumes former class dvd_mod. |
44 with division and modulo operations. Subsumes former class dvd_mod. |