Re: [isabelle] inverse of antiquotations



I have an incantation for taking a thm and making it the goal. You can 
also turn props into trivial thms, for instance:

ML {* val thm = Thm.trivial @{cprop "Suc 0 = 1"} *}

schematic_goal "PROP ?P"
   apply (tactic {* resolve_tac @{context} [thm] 1 *})
   apply ...

Cheers,
     Thomas.

On 13/06/18 15: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.