I just tried
isabelle jedit -R HOL-UNITY
assuming that it would build an auxiliary image for HOL-Auth, which is
imported. It built HOL-Auth rather than HOL-UNITY_requirements(HOL-Auth) so
things are pretty subtle here. A little more explanation would be valuable.
Larry
> On 6 Jun
On 06/06/18 16:19, Lawrence Paulson wrote:
>
> According to the NEWS entry, option -R builds an auxiliary logic image. I
> tried this with a couple of examples and no images were built. According to
> the manual, this option opens the ROOT entry. It does seem to do that, though
> I'm not sure
> On 6 Jun 2018, at 12:43, Makarius wrote:
>
> On 06/06/18 12:45, Lawrence Paulson wrote:
>> I saw them of course, but what do they do?
>
> These options go back to Nov-2017, but in recent Isabelle/bcdc47c9d4af I
> have simplified and clarified the situation, updated NEWS and
> documentation in
On 06/06/18 12:45, Lawrence Paulson wrote:
> I saw them of course, but what do they do?
These options go back to Nov-2017, but in recent Isabelle/bcdc47c9d4af I
have simplified and clarified the situation, updated NEWS and
documentation in the "jedit" manual.
Right now the main question is if
> Am 05.06.2018 um 23:01 schrieb Makarius :
>
> These options are very relevant for the coming release. I am interested
> to get feedback from early adopters, if this is already sufficient or
> requires further refinement.
>
> In other words, the question behind this: Can be get rid of most
>
I saw them of course, but what do they do?
Larry
> On 5 Jun 2018, at 22:19, Makarius wrote:
>
> On 05/06/18 23:06, Lawrence Paulson wrote:
>> I’d find an example helpful, as your brief description is pretty cryptic.
>> Larry
>>
>>> On 5 Jun 2018, at 22:01, Makarius wrote:
>>>
>>> These
On 05/06/18 23:06, Lawrence Paulson wrote:
> I’d find an example helpful, as your brief description is pretty cryptic.
> Larry
>
>> On 5 Jun 2018, at 22:01, Makarius wrote:
>>
>> These options are very relevant for the coming release. I am interested
>> to get feedback from early adopters, if
I’d find an example helpful, as your brief description is pretty cryptic.
Larry
> On 5 Jun 2018, at 22:01, Makarius wrote:
>
> These options are very relevant for the coming release. I am interested
> to get feedback from early adopters, if this is already sufficient or
> requires further
On 04/06/18 14:27, Makarius wrote:
> *** Isabelle/jEdit Prover IDE ***
>
> * The command-line tool "isabelle jedit" provides more flexible options
> for session management:
> - option -R builds an auxiliary logic image with all required theories
> from other sessions, relative to an
*** Isabelle/jEdit Prover IDE ***
* The command-line tool "isabelle jedit" provides more flexible options
for session management:
- option -R builds an auxiliary logic image with all required theories
from other sessions, relative to an ancestor session given by option
-A (default:
10 matches
Mail list logo
