*** 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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
