[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)?



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