equal
deleted
inserted
replaced
137 order of type variables. INCOMPATIBILITY: Tools working with proof |
137 order of type variables. INCOMPATIBILITY: Tools working with proof |
138 terms may need to be adapted. |
138 terms may need to be adapted. |
139 |
139 |
140 |
140 |
141 *** HOL *** |
141 *** HOL *** |
|
142 |
|
143 * Theorem Presburger.int_induct has been renamed to Int.int_bidirectional_induct; |
|
144 theorem Int.int_induct is no longer shadowed. INCOMPATIBILITY. |
142 |
145 |
143 * Dropped theorem duplicate comp_arith; use semiring_norm instead. INCOMPATIBILITY. |
146 * Dropped theorem duplicate comp_arith; use semiring_norm instead. INCOMPATIBILITY. |
144 |
147 |
145 * Theory 'Finite_Set': various folding_* locales facilitate the application |
148 * Theory 'Finite_Set': various folding_* locales facilitate the application |
146 of the various fold combinators on finite sets. |
149 of the various fold combinators on finite sets. |