[isabelle-dev] Advice for replacing @{simpset} with @{context}.

[David Greenaway]

On 13/09/13 04:17, Makarius wrote:
> The NEWS file explains what will happen in the coming release with
> simpset vs. Proof.context -- the Simplifier was one of the last
> hold-outs of non-localized tools, so after long delays we are mostly
> through with it.

Sorry, I should have mentioned that I read the NEWS file; I understood
that the simplifier now accepted a context instead of a simpset, and
that "addsimps" operated on contexts instead of simpsets.

My question was instead related to the best way to perform operations on
long-lived simpsets which need to be mutated over time, now that there
are no exposed APIs for manipulating them.

Florian's reply was helpful in pointing out some code (the code
generator) which also had this problem, and its solution to this which
amounts to: (i) taking your old simpset; (ii) putting it into a dummy
context; (iii) performing your "addsimp"/"addcong"/etc operation; (iv)
extract the simpset out again.

Cheers,
David


________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.