src/HOL/ex/cla.ML

 
 goal HOL.thy "(! x. P(x) & Q(x)) = ((! x. P(x)) & (! x. Q(x)))";
 by (Blast_tac 1);
 result(); 
 
-goal HOL.thy "(? x. P-->Q(x))  =  (P --> (? x.Q(x)))";
-by (Blast_tac 1);
-result(); 
-
-goal HOL.thy "(? x.P(x)-->Q) = ((! x.P(x)) --> Q)";
-by (Blast_tac 1);
-result(); 
-
-goal HOL.thy "((! x.P(x)) | Q)  =  (! x. P(x) | Q)";
+goal HOL.thy "(? x. P-->Q(x))  =  (P --> (? x. Q(x)))";
+by (Blast_tac 1);
+result(); 
+
+goal HOL.thy "(? x. P(x)-->Q) = ((! x. P(x)) --> Q)";
+by (Blast_tac 1);
+result(); 
+
+goal HOL.thy "((! x. P(x)) | Q)  =  (! x. P(x) | Q)";
 by (Blast_tac 1);
 result(); 
 
 (*From Wishnu Prasetya*)
 goal HOL.thy

 by (Blast_tac 1);  
 result();
 
 writeln"Problem 24";
 goal HOL.thy "~(? x. S(x)&Q(x)) & (! x. P(x) --> Q(x)|R(x)) &  \
-\    (~(? x.P(x)) --> (? x.Q(x))) & (! x. Q(x)|R(x) --> S(x))  \
+\    (~(? x. P(x)) --> (? x. Q(x))) & (! x. Q(x)|R(x) --> S(x))  \
 \   --> (? x. P(x)&R(x))";
 by (Blast_tac 1); 
 result();
 
 writeln"Problem 25";

 result();
 
 writeln"Problem 28.  AMENDED";
 goal HOL.thy "(! x. P(x) --> (! x. Q(x))) &   \
 \       ((! x. Q(x)|R(x)) --> (? x. Q(x)&S(x))) &  \
-\       ((? x.S(x)) --> (! x. L(x) --> M(x)))  \
+\       ((? x. S(x)) --> (! x. L(x) --> M(x)))  \
 \   --> (! x. P(x) & L(x) --> M(x))";
 by (Blast_tac 1);  
 result();
 
 writeln"Problem 29.  Essentially the same as Principia Mathematica *11.71";

 \   --> (! x. S(x))";
 by (Blast_tac 1);  
 result();
 
 writeln"Problem 31";
-goal HOL.thy "~(? x.P(x) & (Q(x) | R(x))) & \
+goal HOL.thy "~(? x. P(x) & (Q(x) | R(x))) & \
 \       (? x. L(x) & P(x)) & \
 \       (! x. ~ R(x) --> M(x))  \
 \   --> (? x. L(x) & M(x))";
 by (Blast_tac 1);
 result();

 by (Blast_tac 1);
 result();
 
 writeln"Problem 37";
 goal HOL.thy "(! z. ? w. ! x. ? y. \
-\          (P x z -->P y w) & P y z & (P y w --> (? u.Q u w))) & \
+\          (P x z -->P y w) & P y z & (P y w --> (? u. Q u w))) & \
 \       (! x z. ~(P x z) --> (? y. Q y z)) & \
 \       ((? x y. Q x y) --> (! x. R x x))  \
 \   --> (! x. ? y. R x y)";
 by (Blast_tac 1);
 result();

 
 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 HOL.thy "(? x y::'a. ! z. z=x | z=y) & P(a) & P(b) & (~a=b) \
-\               --> (! u::'a.P(u))";
+\               --> (! u::'a. P(u))";
 by (Classical.safe_tac (!claset));
 by (res_inst_tac [("x","a")] allE 1);
 by (assume_tac 1);
 by (res_inst_tac [("x","b")] allE 1);
 by (assume_tac 1);
 by (Blast_tac 1);
 result();
 
 writeln"Problem 50";  
 (*What has this to do with equality?*)
-goal HOL.thy "(! x. P a x | (! y.P x y)) --> (? x. ! y.P x y)";
+goal HOL.thy "(! x. P a x | (! y. P x y)) --> (? x. ! y. P x y)";
 by (Blast_tac 1);
 result();
 
 writeln"Problem 51";
 goal HOL.thy