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