Re: [isabelle] Storing data in a locale



Hi Gudmund,

I thought I could use Proof_Data and local_setup as illustrated in the
following code snippet:

local_setup is rather non-standard. Grep tells me that it is currently unused in the entire Isabelle distribution, and I don't actually know what it is good for...

Instead, I think you should use a "declaration".

declaration {* fn _ => Context.map_proof (set_numbs 2) *}

Note that the extra argument _ is a morphism, since the declaration also affects interpretations of the locale. If you have something more interesting data than just numbers, you may want to apply the morphism to it.

Hope this helps...

Alex





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