On Fri, 13 Sep 2013, Peter Lammich wrote:
The relevant text from NEWS is this:
* 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.
So the only way to replace a "HOL_basic_ss addsimps ..." somewhere deep
inside my code (in my actual case, inside a conversion) is to thread
through the proof context everywhere? ... a quite tedious change.
Is this hypothetical, or do you still have tools without a proper context?
It should be trivial to pass through some ctxt: Proof.context nonetheless,
i.e. do the "localization" in that elementary sense. Unless there is
something really strange here ...
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
