Re: [isabelle] antiquotations

Hi Dominique,

Thanks - that's most helpful.  Do you know if this is documented anywhere?



On 06/04/2018 11:05 PM, Dominique Unruh wrote:

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,

On 4 June 2018 at 07:12, Lars Hupel <hupel at <mailto:hupel at>> 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.


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