[isabelle] inverse of antiquotations



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.