--- a/src/FOL/ex/Nat.ML Sat Sep 03 16:50:22 2005 +0200
+++ b/src/FOL/ex/Nat.ML Sat Sep 03 17:15:51 2005 +0200
@@ -9,8 +9,6 @@
Pretty.setmargin 72; print_depth 0;
*)
-open Nat;
-
Goal "Suc(k) ~= k";
by (res_inst_tac [("n","k")] induct 1);
by (rtac notI 1);