NEWS
changeset 17597 dac8dd2272cd
parent 17595 3e3a30bf702f
child 17619 026f7bbc8a0f
equal deleted inserted replaced
17596:cd555d5a3254 17597:dac8dd2272cd
   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 /