[isabelle] using files




I find that sometimes (unpredictably) "use"ing a file uses the "wrong" file, for example in the src/HOL directory,

ThyLoad.show_path();
> val it = ["."] : string list

 Library.pwd () ;
 > val it = "/home/users/jeremy/Isabelle2005/src/HOL" : string

ThyInfo.use "ROOT.ML"; (* uses Pure/ROOT.ML *)

What exactly does ThyInfo.use do to decide what file to use?

thanks,

Jeremy






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