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