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.

Cheers

Chunqing


You use add_path, eg


add_path "../gen05" ;
or
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.

Regards,

Jeremy





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.