Re: [isabelle] novice problem about loading theorey file

Chen Chunqing wrote:
Dear all,

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 MHonArc.