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