Re: [isabelle] novice problem about loading theorey file
On Fri, 25 Nov 2005, Jeremy Dawson wrote:
> 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.
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and