# HG changeset patch # User nipkow # Date 1127427058 -7200 # Node ID 56dc95e8b5c563bebb76bb53ce72bbd6b495f166 # Parent 58eeffd73be1953bd4d558d2d47d89d2b17d915e *** empty log message *** diff -r 58eeffd73be1 -r 56dc95e8b5c5 NEWS --- a/NEWS Thu Sep 22 23:56:15 2005 +0200 +++ b/NEWS Fri Sep 23 00:10:58 2005 +0200 @@ -225,6 +225,8 @@ or ==>. More generally, erule now works even if the major premise of the elimination rule contains !! or ==>. +* Method "rules" has been renamed to "iprover" + * Reorganized bootstrapping of the Pure theories; CPure is now derived from Pure, which contains all common declarations already. Both theories are defined via plain Isabelle/Isar .thy files. diff -r 58eeffd73be1 -r 56dc95e8b5c5 TODO --- a/TODO Thu Sep 22 23:56:15 2005 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,14 +0,0 @@ -For Isabelle2005: - -- update course material slides to new theory headers (Tobias) - -- Library/ExecutableSet.thy (Stefan) - -- a global "disprove" menu item both as an action and (if it can be done) - as a setting (Stefan & Tjark) - -- convert fast_lin_arith.ML and cooper_dec.ML to use IntInf (Tobias) - -- ball, bex and setsum congruence rules (Tobias & Stefan) - -- remove this file (Tobias)