Re: [isabelle] inverse of antiquotations



There is this thread from a few years ago:
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2015-June/msg00076.html

Cheers,

Manuel


On 13/06/18 07:01, Jeremy Dawson wrote:
> On 06/05/2018 07:53 PM, Makarius wrote:
>>    ML_val ‹@{Isar.goal}›
> 
> Conversely, if you have a term (or theorem or text string, etc) as an ML
> value, how to you set it as the new goal (as in, eg, the lemma Isar
> command)?
> 
> Thanks
> 
> Jeremy
> 




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