--- a/src/FOL/ex/Nat.ML Thu Oct 07 09:47:47 1993 +0100
+++ b/src/FOL/ex/Nat.ML Thu Oct 07 09:49:46 1993 +0100
@@ -15,7 +15,7 @@
open Nat;
-goal Nat.thy "~ (Suc(k) = k)";
+goal Nat.thy "Suc(k) ~= k";
by (res_inst_tac [("n","k")] induct 1);
by (resolve_tac [notI] 1);
by (eresolve_tac [Suc_neq_0] 1);