(* test file *) theory Test use import prelude.Int logic id(x: int) : int = x logic even(x: int) = 2*(x/2) = x goal G : forall x:int. 0 = 0 goal G2 : forall x:int. 0 = 1 end (* Local Variables: compile-command: "make -C .. test" End: *)