Re: [isabelle] novice problem about loading theorey file

On Fri, 25 Nov 2005, Jeremy Dawson wrote:

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

What do you mean by properly?  Changing the load path during an incomplete
load is not a well-defined operation.  The behaviour is unspecified, i.e.  
there is no bug here.

> But I have it working by running these commands before loading any
> theory.

Good idea.


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