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