Email Gateway (Aug 22 2022 at 17:35): Email Gateway (Aug 22 2022 at 17:35):From: Jeremy Dawson <Jeremy.Dawson@anu.edu.au>
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
Email Gateway (Aug 22 2022 at 17:35):From: Thomas.Sewell@data61.csiro.au
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.
Email Gateway (Aug 22 2022 at 17:35):From: Manuel Eberl <eberlm@in.tum.de>
There is this thread from a few years ago:
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2015-June/msg00076.html
Cheers,
Manuel
Email Gateway (Aug 22 2022 at 17:35):From: Jeremy Dawson <Jeremy.Dawson@anu.edu.au>
Hi Thomas,
Thanks very much - very clever! And most useful.
Cheers,
Jeremy
Last updated: Apr 25 2024 at 04:18 UTC