NEWS
changeset 42793 88bee9f6eec7
parent 42740 31334a7b109d
child 42809 5b45125b15ba
     1.1 --- a/NEWS	Fri May 13 16:03:03 2011 +0200
     1.2 +++ b/NEWS	Fri May 13 22:55:00 2011 +0200
     1.3 @@ -144,6 +144,14 @@
     1.4  * Slightly more special eq_list/eq_set, with shortcut involving
     1.5  pointer equality (assumes that eq relation is reflexive).
     1.6  
     1.7 +* Classical tactics use proper Proof.context instead of historic types
     1.8 +claset/clasimpset.  Old-style declarations like addIs, addEs, addDs
     1.9 +operate directly on Proof.context.  Raw type claset retains its use as
    1.10 +snapshot of the classical context, which can be recovered via
    1.11 +(put_claset HOL_cs) etc.  Type clasimpset has been discontinued.
    1.12 +INCOMPATIBILITY, classical tactics and derived proof methods require
    1.13 +proper Proof.context.
    1.14 +
    1.15  
    1.16  
    1.17  New in Isabelle2011 (January 2011)