Re: [isabelle] Named_Target.reinit

On Wed, 23 Jul 2014, Lars Noschinski wrote:

I see that Named_Target.reinit is gone in 2014-rc0. It seems that it is equivalent to leaving to a theory and then entering the target again. What was its purpose and what is the right way to replace it?

This belongs to the system infrastructure -- user-space tools in Isabelle/ML should not be affected by the change.

It seems that it is sometimes necessary to perform these steps to get the simpset updated after changing it in the background theory with Local_Theory.background_theory_result.

This sounds a bit odd, maybe some formerly global-theory tool that was updated a bit too quickly, without really leaving the old ways behind.

Declarations with the "simp" attribute may be done like in Isar source, using the ML antiquotation @{attributes [simp]} with Local_Theory.note, for example. (Just hypersearch the sources for examples.)

If the simpset update is some other ML function, not an attribute, you may use Simplifier.map_ss with Local_Theory.declaration, which also allows to insist in a pervasive scope, such that the declaration affects the global theory as well.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.