equal
deleted
inserted
replaced
223 |
223 |
224 * thin_tac now works even if the assumption being deleted contains !! |
224 * thin_tac now works even if the assumption being deleted contains !! |
225 or ==>. More generally, erule now works even if the major premise of |
225 or ==>. More generally, erule now works even if the major premise of |
226 the elimination rule contains !! or ==>. |
226 the elimination rule contains !! or ==>. |
227 |
227 |
228 * Method "rules" has been renamed to "iprover" |
228 * Method 'rules' has been renamed to 'iprover'. INCOMPATIBILITY. |
229 |
229 |
230 * Reorganized bootstrapping of the Pure theories; CPure is now derived |
230 * Reorganized bootstrapping of the Pure theories; CPure is now derived |
231 from Pure, which contains all common declarations already. Both |
231 from Pure, which contains all common declarations already. Both |
232 theories are defined via plain Isabelle/Isar .thy files. |
232 theories are defined via plain Isabelle/Isar .thy files. |
233 INCOMPATIBILITY: elements of CPure (such as the CPure.intro / |
233 INCOMPATIBILITY: elements of CPure (such as the CPure.intro / |