[isabelle-dev] NEWS: simplifier context

[Makarius]

* Simplifier tactics and tools use proper Proof.context instead of
historic type simpset.  Old-style declarations like addsimps,
addsimprocs etc. operate directly on Proof.context.  Raw type simpset
retains its use as snapshot of the main Simplifier context, using
simpset_of and put_simpset on Proof.context.  INCOMPATIBILITY -- port
old tools by making them depend on (ctxt : Proof.context) instead of
(ss : simpset), then turn (simpset_of ctxt) into ctxt.

* Discontinued obsolete ML antiquotations @{claset} and @{simpset}.
INCOMPATIBILITY, use @{context} instead.


This refers to Isabelle/0c944215934a and AFP/14ae137e23b6.

It should end the anomalies introduced by simpset vs. Proof.context 
competing for the notion of "the context".  Tools that are part of the 
Classical reasoner, Simplifier etc. can now pass the Proof.context back 
and forth without loss of information (fixed variables, "bounds", "prems" 
etc.) so that odd warnings about variable clashes should disappear 
eventually.


 	Makarius