--- 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);
--- a/src/FOL/ex/cla.ML Thu Oct 07 09:47:47 1993 +0100
+++ b/src/FOL/ex/cla.ML Thu Oct 07 09:49:46 1993 +0100
@@ -363,10 +363,9 @@
\ --> (ALL y. g(y) & h(x,y) --> k(y))) & \
\ ~ (EX y. l(y) & k(y)) & \
\ (EX x. f(x) & (ALL y. h(x,y) --> l(y)) \
-\ & (ALL y. g(y) & h(x,y) --> j(x,y))) \
+\ & (ALL y. g(y) & h(x,y) --> j(x,y))) \
\ --> (EX x. f(x) & ~ (EX y. g(y) & h(x,y)))";
by (best_tac FOL_cs 1);
-(*41.5 secs*)
result();
@@ -380,7 +379,7 @@
writeln"Problem 49 NOT PROVED AUTOMATICALLY";
(*Hard because it involves substitution for Vars;
the type constraint ensures that x,y,z have the same type as a,b,u. *)
-goal FOL.thy "(EX x y::'a. ALL z. z=x | z=y) & P(a) & P(b) & (~a=b) \
+goal FOL.thy "(EX x y::'a. ALL z. z=x | z=y) & P(a) & P(b) & a~=b \
\ --> (ALL u::'a.P(u))";
by (safe_tac FOL_cs);
by (res_inst_tac [("x","a")] allE 1);
--- 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);