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 [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
