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




> On 6 Jun 2021, at 20:19, Makarius <makarius at sketis.net> wrote:
> 
> On 06/06/2021 02:35, Gerwin Klein wrote:
>> 
>>> On 6 Jun 2021, at 06:00, Makarius <makarius at sketis.net> 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.

Cheers,
Gerwin





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