[isabelle-dev] Extracting dependencies from theory headers

[Gerwin Klein]

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.

Cheers,
Gerwin