[isabelle-dev] Two problems

[Jasmin Christian Blanchette]

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