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