[isabelle-dev] Two problems

Jasmin Christian Blanchette jasmin.blanchette at gmail.com
Mon Dec 3 22:55:27 CET 2012

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.


More information about the isabelle-dev mailing list