[isabelle-dev] Extracting dependencies from theory headers
matthews at galois.com
Wed Dec 22 00:24:19 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.
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?
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 2205 bytes
Desc: not available
More information about the isabelle-dev