[isabelle-dev] Extracting dependencies from theory headers

Gerwin Klein gerwin.klein at nicta.com.au
Tue Dec 21 22:42:58 CET 2010

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 toplevel

Seconded. This causes quite a bit of confusion every time new users come in.


More information about the isabelle-dev mailing list