[isabelle-dev] Two problems

[Lawrence Paulson]

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?

Larry

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