--- a/IOA/ROOT.ML Sun Nov 06 21:04:39 1994 +0100 +++ b/IOA/ROOT.ML Sun Nov 06 21:04:50 1994 +0100 @@ -1,4 +1,4 @@ goals_limit := 1; -loadpath := "./meta_theory" :: "./example" :: !loadpath; +loadpath := "IOA/meta_theory" :: "IOA/example" :: !loadpath; use_thy "Correctness";