Re: [isabelle] antiquotations



Hi Dominique,

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

Cheers,

Jeremy

On 06/04/2018 11:05 PM, Dominique Unruh wrote:
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 <mailto: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.