Re: [isabelle] making local definitions programmatically



Florian Haftmann wrote:

> Concerning this, recall the following:

>>>> locale L =
>>>>   fixes c0 :: "'a \<Rightarrow> 'a"
>>>> begin
>>>>
>>>> ML {*
>>>> fun def lthy =
>>>>   let
>>>>     val ((t, _), lthy') = LocalTheory.define Thm.definitionK
>>>> (("c1", NoSyn), (("", []), @{term "\<lambda>x. c0 (c0 x)"})) lthy;
>>>>     val lthy'' = LocalTheory.restore lthy';
>>>> val t' = Morphism.term (ProofContext.export_morphism lthy' lthy'') t;
>>>>   in (t', lthy'') end;
>>>> *}
>>>>
>>>> ML {*
>>>> Context.>>> (Context.map_proof_result def)
>>>> *}

> This approach refrains from assuming anything about a particular
> naming policy.

Ah yes.  If I call LocalTheory.restore, I guess I still have to later
call LocalTheory.exit.  Is that right?

And another thing: a while back Makarius said that we should avoid all
functions that implicitly manipulate references because these are
unsafe in the presence of threads.  Yet it is clear that Context.>>>
must be doing this.  Is this function an exception to the general rule?

Thanks,
Michael.





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