[isabelle] antiquotations




Hi

I don't seem to be able to use the goals or subgoals antiquotations correctly

lemma example: "a = b --> b = a"
ML_prf {* @{thm refl} *}

ML_prf {* @{goals} *} (* fails *)
ML_prf {* @{subgoals} *} (* fails *)
ML_prf {* @{context} *} (* OK *)
ML_prf {* @{theory} *} (* OK *)

what am I doing wrong here?

Thanks

Jeremy




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