1 goals_limit := 1;
2
3 loadpath := "./meta_theory" :: "./example" :: !loadpath;
3 loadpath := "IOA/meta_theory" :: "IOA/example" :: !loadpath;
4 use_thy "Correctness";