[isabelle-dev] NEWS: classical tactics use Proof.context (f092945f0ef7)

[Makarius]

*** ML ***

* Classical tactics use proper Proof.context instead of historic types
claset/clasimpset.  Old-style declarations like addIs, addEs, addDs
operate directly on Proof.context.  Raw type claset retains its use as
snapshot of the classical context, which can be recovered via
(put_claset HOL_cs) etc.  Type clasimpset has been discontinued.
INCOMPATIBILITY, classical tactics and derived proof methods require
proper Proof.context.


 	Makarius