[isabelle-dev] Two problems

Lawrence Paulson lp15 at cam.ac.uk
Mon Dec 3 23:08:52 CET 2012

Surely the existence of two theories of the same name can be detected?

JEdit has been working fine for me for the past couple of weeks (despite updating regularly and getting new versions). Missing components maybe?


On 3 Dec 2012, at 21:55, Jasmin Christian Blanchette <jasmin.blanchette at gmail.com> wrote:

> Am 03.12.2012 um 22:31 schrieb Jasmin Christian Blanchette:
>> I'd like to report two problems with Isabelle (b17b05c8d4a4) -- AFP (40ecbad14077).
>> 1. In Proof General:
>>   theory Scratch
>>   imports
>>     "$MY_AFP_DEVEL_HOME/thys/Jinja/J/TypeSafe"
>>     "~~/src/HOL/Proofs/Lambda/StrongNorm"
>>   begin
> I investigated some more, and this problem is clearly related to the existence of two theories called "Type.thy" -- which one gets picked up depends on luck. So I guess that's a known issue.
> Jasmin
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

More information about the isabelle-dev mailing list