Re: [isabelle] inverse of antiquotations



Hi Thomas,

Thanks very much - very clever!  And most useful.

Cheers,

Jeremy

On 06/13/2018 03:11 PM, Thomas.Sewell at data61.csiro.au wrote:
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.