Re: [isabelle] Storing data in a locale



Alex

Thanks - it was exactly what I needed.

Gudmund

On 28 May 2011, at 11:17, Alexander Krauss wrote:

> 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
> 


-- 
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.






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