Re: [isabelle] antiquotation for the current goal



> For @{Isar.goal} see
> http://isabelle.in.tum.de/dist/Isabelle2013/doc/implementation.pdf page
> 112:
>
>    @{text "@{Isar.goal}"} refers to the regular goal state (if
>    available) of the current proof state managed by the Isar toplevel
>    --- as abstract value.
>
>    This only works for diagnostic ML commands, such as @{command
>    ML_val} or @{command ML_command}.

That's great that the antiquotation works. Unfortunately, it still doesn't fit into my use case.

My use case is the following:
lemma "bla"
apply sth
ML_prf{*
  val goal = @{Isar.goal}
  val rules = do_sth_complicated goal
*}
apply (tactic {* rtac rules 1 *})

If I am allowed to use @{Isar.goal} only inside of ML_val, I cannot see the variable "rules" outside of the ML block. Is there any deep reason why @{Isar.goal} can be used only inside of ML_val and not in ML_prf? Allowing @{Isar.goal} inside of ML_prf would help me to do debugging in Isabelle. It's basically about moving parts of F from "apply (tactic {* F *})" to a ML_prf block as much as possible and inspecting intermediate results in the Output window. This gives me more flexibility than cluttering F with print statements and inspecting the printed stuff.

Best,
Ondrej




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