Re: [isabelle] antiquotations



Hi,

you can use

lemma example: "a = b --> b = a"
  ML_val {* @{Isar.goal} *}

to get the current goal. Note though, that this does not work with ML_prf.

Best wishes,
Dominique.






On 4 June 2018 at 07:12, Lars Hupel <hupel at in.tum.de> wrote:

> 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.