Re: [isabelle] making local definitions programmatically



Florian Haftmann wrote:
>> ML {* val t = Syntax.check_term @{context} (Const("local.c1", dummyT))
>>       val ctxt' = LocalTheory.define Thm.definitionK
>>                                      (("c3", NoSyn), (("", []), t))
>>                                      @{context}
>> *}

> Which Isabelle version are you using?  The following works fine with
> Isabelle2007 [...]

I just tried it again; and now it works.  This is very strange, but
I'll assume I messed up my previous experiment.  Thanks for your help!

Michael.





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