Re: [isabelle] The instructions in AFP's "Using Entries" do not work
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.
There is another ongoing process of rethinking: how to allow Isabelle/Scala
modules within sessions and/or components.
Maybe I eventually get the right idea, when revisiting this more seriously.
This archive was generated by a fusion of
Pipermail (Mailman edition) and