equal
deleted
inserted
replaced
80 without introducing dependencies on parameters or assumptions, which |
80 without introducing dependencies on parameters or assumptions, which |
81 is not possible in Isabelle/Pure. |
81 is not possible in Isabelle/Pure. |
82 |
82 |
83 |
83 |
84 *** HOL *** |
84 *** HOL *** |
|
85 |
|
86 * Split off theory Big_Operators containing setsum, setprod, Inf_fin, Sup_fin, |
|
87 Min, Max from theory Finite_Set. INCOMPATIBILITY. |
85 |
88 |
86 * Theory "Rational" renamed to "Rat", for consistency with "Nat", "Int" etc. |
89 * Theory "Rational" renamed to "Rat", for consistency with "Nat", "Int" etc. |
87 INCOMPATIBILITY. |
90 INCOMPATIBILITY. |
88 |
91 |
89 * New set of rules "ac_simps" provides combined assoc / commute rewrites |
92 * New set of rules "ac_simps" provides combined assoc / commute rewrites |