# HG changeset patch
# User lcp
# Date 749983786 -3600
# Node ID 70c6014c9b6f795f290abeefd4a9d746edbbe8e8
# Parent  d71f96f1780eb81f69d36966f31a6b1898e17dd6
examples now use ~= for "not equals"

diff -r d71f96f1780e -r 70c6014c9b6f src/FOL/ex/Nat.ML
--- 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);
diff -r d71f96f1780e -r 70c6014c9b6f src/FOL/ex/cla.ML
--- 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);
diff -r d71f96f1780e -r 70c6014c9b6f src/FOL/ex/nat.ML
--- 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);