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