Re: [isabelle] antiquotations



Dear Jeremy,

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

as far as I understand, those are "document antiquotations", i.e. they
may only appear in document text, but not in ML:

  text ‹@{goals}›

If you want to take a look at the proof state from within the IDE, you
have two choices:

1) open the "State" panel
2) open the "Output" panel and check the "Proof state" box

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

Note that this can be shorter expressed as "thm refl" directly. No need
to wrap that into ML.

Cheers
Lars




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