Re: [isabelle] inverse of antiquotations

There is this thread from a few years ago:



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.