NEWS
changeset 30609 983e8b6e4e69
parent 30577 79cc595655c0
child 30706 e20227b5e6a3
     1.1 --- a/NEWS	Fri Mar 20 17:04:44 2009 +0100
     1.2 +++ b/NEWS	Fri Mar 20 17:12:37 2009 +0100
     1.3 @@ -685,6 +685,12 @@
     1.4  Syntax.read_term_global etc.; see also OldGoals.read_term as last
     1.5  resort for legacy applications.
     1.6  
     1.7 +* Disposed old declarations, tactics, tactic combinators that refer to
     1.8 +the simpset or claset of an implicit theory (such as Addsimps,
     1.9 +Simp_tac, SIMPSET).  INCOMPATIBILITY, should use @{simpset} etc. in
    1.10 +embedded ML text, or local_simpset_of with a proper context passed as
    1.11 +explicit runtime argument.
    1.12 +
    1.13  * Antiquotations: block-structured compilation context indicated by
    1.14  \<lbrace> ... \<rbrace>; additional antiquotation forms:
    1.15