Re: [isabelle] The instructions in AFP's "Using Entries" do not work

> On 6 Jun 2021, at 20:19, Makarius <makarius at> wrote:
> On 06/06/2021 02:35, Gerwin Klein wrote:
>>> On 6 Jun 2021, at 06:00, Makarius <makarius at> wrote:
>>> The option -d '$AFP' has later become idiomatic for many other Isabelle tools,
>>> to add the "AFP aspect" with minimal complexity. For example for the Prover IDE:
>>> isabelle jedit -d '$AFP'
>> Agree, that was the canonical way, but that was part of the problem. It doesn't work for users who don't use the command line.
> Yes, I am aware of that extra assumption. It is part of the process to rethink
> AFP within the Prover IDE.

Integrating the AFP more will probably be the better way long-term, yes.


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