Re: [isabelle] novice problem about loading theorey file
Chen Chunqing wrote:
Can anyone teach me how to load an established theory file which is not
in the same directory? Thanks in advance.
You use add_path, eg
add_path "../gen05" ;
add_path "$ISABELLE_HOME_USER/gen05" ;
Also show_path() is useful.
Note that there is a bug introduced into Isabelle2005
whereby doing this in an ML file loaded by doing use_thy for another
theory doesn't seem to work properly
But I have it working by running these commands before loading any theory.
This archive was generated by a fusion of
Pipermail (Mailman edition) and