# HG changeset patch
# User paulson
# Date 909046698 -7200
# Node ID 81e1a83ee00265e48838f1b1d8ec7e5fb100e156
# Parent  c669e2161b089f190ca80c6ad652a749834e7e5f
tidying

diff -r c669e2161b08 -r 81e1a83ee002 src/FOL/ex/cla.ML
--- a/src/FOL/ex/cla.ML	Thu Oct 22 10:57:18 1998 +0200
+++ b/src/FOL/ex/cla.ML	Thu Oct 22 10:58:18 1998 +0200
@@ -143,8 +143,7 @@
 
 (*Discussed in Avron, Gentzen-Type Systems, Resolution and Tableaux,
   JAR 10 (265-281), 1993.  Proof is trivial!*)
-Goal
-    "~ ((EX x.~P(x)) & ((EX x. P(x)) | (EX x. P(x) & Q(x))) & ~ (EX x. P(x)))";
+Goal "~ ((EX x.~P(x)) & ((EX x. P(x)) | (EX x. P(x) & Q(x))) & ~ (EX x. P(x)))";
 by (Blast_tac 1);
 result();
 
@@ -306,8 +305,7 @@
 result();
 
 writeln"Problem 36";
-Goal
-     "(ALL x. EX y. J(x,y)) & \
+Goal "(ALL x. EX y. J(x,y)) & \
 \     (ALL x. EX y. G(x,y)) & \
 \     (ALL x y. J(x,y) | G(x,y) --> (ALL z. J(y,z) | G(y,z) --> H(x,z)))   \
 \ --> (ALL x. EX y. H(x,y))";
@@ -324,8 +322,7 @@
 result();
 
 writeln"Problem 38";
-Goal
-    "(ALL x. p(a) & (p(x) --> (EX y. p(y) & r(x,y))) -->        \
+Goal "(ALL x. p(a) & (p(x) --> (EX y. p(y) & r(x,y))) -->        \
 \            (EX z. EX w. p(z) & r(x,w) & r(w,z)))  <->         \
 \    (ALL x. (~p(a) | p(x) | (EX z. EX w. p(z) & r(x,w) & r(w,z))) &    \
 \            (~p(a) | ~(EX y. p(y) & r(x,y)) |                          \
@@ -385,8 +382,7 @@
 
 
 writeln"Problem 46";
-Goal
-    "(ALL x. f(x) & (ALL y. f(y) & h(y,x) --> g(y)) --> g(x)) &      \
+Goal "(ALL x. f(x) & (ALL y. f(y) & h(y,x) --> g(y)) --> g(x)) &      \
 \    ((EX x. f(x) & ~g(x)) -->                                    \
 \     (EX x. f(x) & ~g(x) & (ALL y. f(y) & ~g(y) --> j(x,y)))) &    \
 \    (ALL x y. f(x) & f(y) & h(x,y) --> ~j(y,x))                    \
@@ -422,16 +418,14 @@
 result();
 
 writeln"Problem 51";
-Goal
-    "(EX z w. ALL x y. P(x,y) <->  (x=z & y=w)) -->  \
+Goal "(EX z w. ALL x y. P(x,y) <->  (x=z & y=w)) -->  \
 \    (EX z. ALL x. EX w. (ALL y. P(x,y) <-> y=w) <-> x=z)";
 by (Blast_tac 1);
 result();
 
 writeln"Problem 52";
 (*Almost the same as 51. *)
-Goal
-    "(EX z w. ALL x y. P(x,y) <->  (x=z & y=w)) -->  \
+Goal "(EX z w. ALL x y. P(x,y) <->  (x=z & y=w)) -->  \
 \    (EX w. ALL y. EX z. (ALL x. P(x,y) <-> x=z) <-> y=w)";
 by (Blast_tac 1);
 result();
@@ -439,8 +433,7 @@
 writeln"Problem 55";
 
 (*Original, equational version by Len Schubert, via Pelletier *** NOT PROVED
-Goal
-  "(EX x. lives(x) & killed(x,agatha)) & \
+Goal "(EX x. lives(x) & killed(x,agatha)) & \
 \  lives(agatha) & lives(butler) & lives(charles) & \
 \  (ALL x. lives(x) --> x=agatha | x=butler | x=charles) & \
 \  (ALL x y. killed(x,y) --> hates(x,y)) & \
@@ -472,19 +465,18 @@
 \  (ALL x. hates(agatha,x) --> hates(butler,x)) & \
 \  (ALL x. ~hates(x,agatha) | ~hates(x,butler) | ~hates(x,charles)) --> \
 \   killed(?who,agatha)";
-by (Fast_tac 1);  (*MUCH faster than Blast_tac: 8s against 29s*)
+by (Fast_tac 1);  
+  (*MUCH faster than Blast_tac: 1.5s against ??s, mostly proof reconstruction*)
 result();
 
 
 writeln"Problem 56";
-Goal
-    "(ALL x. (EX y. P(y) & x=f(y)) --> P(x)) <-> (ALL x. P(x) --> P(f(x)))";
+Goal "(ALL x. (EX y. P(y) & x=f(y)) --> P(x)) <-> (ALL x. P(x) --> P(f(x)))";
 by (Blast_tac 1);
 result();
 
 writeln"Problem 57";
-Goal
-    "P(f(a,b), f(b,c)) & P(f(b,c), f(a,c)) & \
+Goal "P(f(a,b), f(b,c)) & P(f(b,c), f(a,c)) & \
 \    (ALL x y z. P(x,y) & P(y,z) --> P(x,z))    -->   P(f(a,b), f(a,c))";
 by (Blast_tac 1);
 result();
@@ -500,14 +492,12 @@
 result();
 
 writeln"Problem 60";
-Goal
-    "ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))";
+Goal "ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))";
 by (Blast_tac 1);
 result();
 
 writeln"Problem 62 as corrected in JAR 18 (1997), page 135";
-Goal
-    "(ALL x. p(a) & (p(x) --> p(f(x))) --> p(f(f(x))))  <->     \
+Goal "(ALL x. p(a) & (p(x) --> p(f(x))) --> p(f(f(x))))  <->     \
 \    (ALL x. (~p(a) | p(x) | p(f(f(x)))) &                      \
 \            (~p(a) | ~p(f(x)) | p(f(f(x)))))";
 by (Blast_tac 1);
@@ -523,8 +513,7 @@
 
 (*From Rudnicki, Obvious Inferences, JAR 3 (1987), 383-393.  
   It does seem obvious!*)
-Goal
-    "(ALL x. F(x) & ~G(x) --> (EX y. H(x,y) & J(y))) &        \
+Goal "(ALL x. F(x) & ~G(x) --> (EX y. H(x,y) & J(y))) &        \
 \    (EX x. K(x) & F(x) & (ALL y. H(x,y) --> K(y)))  &        \
 \    (ALL x. K(x) --> ~G(x))   -->   (EX x. K(x) --> ~G(x))";
 by (Fast_tac 1);
@@ -532,8 +521,7 @@
 
 (*Halting problem: Formulation of Li Dafa (AAR Newsletter 27, Oct 1994.)
 	author U. Egly*)
-Goal
- "((EX x. A(x) & (ALL y. C(y) --> (ALL z. D(x,y,z)))) -->               \
+Goal "((EX x. A(x) & (ALL y. C(y) --> (ALL z. D(x,y,z)))) -->               \
 \  (EX w. C(w) & (ALL y. C(y) --> (ALL z. D(w,y,z)))))                  \
 \ &                                                                     \
 \ (ALL w. C(w) & (ALL u. C(u) --> (ALL v. D(w,u,v))) -->                \
@@ -555,8 +543,7 @@
 
 
 (*Halting problem II: credited to M. Bruschi by Li Dafa in JAR 18(1), p.105*)
-Goal
- "((EX x. A(x) & (ALL y. C(y) --> (ALL z. D(x,y,z)))) -->       \
+Goal "((EX x. A(x) & (ALL y. C(y) --> (ALL z. D(x,y,z)))) -->       \
 \  (EX w. C(w) & (ALL y. C(y) --> (ALL z. D(w,y,z)))))          \
 \ &                                                             \
 \ (ALL w. C(w) & (ALL u. C(u) --> (ALL v. D(w,u,v))) -->        \