[isabelle] Storing data in a locale



Dear all,

I am trying to store some data in the context of a locale which I can
later extract when working in that particular locale.

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

ML{*
structure Numbs = Proof_Data(type T = int fun init _ =  1);
val set_numbs = Numbs.map o K;
val get_numbs = Numbs.get;
*}

locale test
begin
 local_setup{* set_numbs 2 *}
end

lemma (in test) "True"
 ML_prf{* get_numbs @{context} *}
oops

However, get_numbs returns (the initial) 1 and not 2 as I would expect.

Does anyone know how I can achieve this?

Cheers,

Gudmund

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