Re: [isabelle] antiquotations



I don't know if it's documented. I found it via autocompletion in
Isabelle/jEdit. But it took some experimenting to figure out that it works
with ML_val. (Because otherwise it just thrown UNDEF).

Best wishes,
Dominique.


On 4 June 2018 at 11:28, Jeremy Dawson <Jeremy.Dawson at anu.edu.au> wrote:

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