Hello all, I recently discovered that warnings about the secondard search path are generated more often than they ought to be. I am using repository version 1fa4725c4656.
Create two files A.thy and B.thy with the following contents: theory A imports "~~/src/HOL/Library/Cardinality" begin end theory B imports A begin end Theory A loads an arbitrary file from HOL/Library, which is included in the legacy default search path, although the full path is given here to avoid the "Legacy feature" warning. If I load theory A by itself in ProofGeneral, it imports Cardinality.thy without warning. Similarly, if I load theory B by itself in ProofGeneral, there is no warning. But if I have both A.thy and B.thy open in ProofGeneral, step through A.thy first, and *then* start stepping through B.thy, I get the following warning when I import A from B: ### Legacy feature! File "Cardinality.thy" located via secondary search path: "$ISABELLE_HOME/src/HOL/Library Can anyone explain this behavior? - Brian _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
