Hi Gerwin,
On 22/12/2010, at 2:52 AM, Lars Noschinski wrote:Furthermore, I would argue that current_dir should not be part of the load_path while recursively loading dependencies. The only time current_dir should be considered is when loading a theory file "from the toplevelSeconded. This causes quite a bit of confusion every time new users come in.
I'm not quite sure what "recursive dependencies" means here. However I think it's important to support the use-case where a new-ish user decides to split their single theory into two or more separate theories in the same directory and have one theory import the others. Would this still be supported?
-john
smime.p7s
Description: S/MIME cryptographic signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
