--- a/src/ZF/AC/WO6_WO1.ML Thu Jan 13 17:30:23 2000 +0100
+++ b/src/ZF/AC/WO6_WO1.ML Thu Jan 13 17:31:30 2000 +0100
@@ -57,10 +57,10 @@
(* Two cases for lemma ii *)
(* ********************************************************************** *)
Goalw [lesspoll_def]
- "!! a f u. ALL b<a. ALL g<a. ALL d<a. u(f,b,g,d) lepoll m ==> \
-\ (ALL b<a. f`b ~= 0 --> (EX g<a. EX d<a. u(f,b,g,d) ~= 0 & \
-\ u(f,b,g,d) lesspoll m)) | \
-\ (EX b<a. f`b ~= 0 & (ALL g<a. ALL d<a. u(f,b,g,d) ~= 0 --> \
+ "ALL b<a. ALL g<a. ALL d<a. u(f,b,g,d) lepoll m \
+\ ==> (ALL b<a. f`b ~= 0 --> \
+\ (EX g<a. EX d<a. u(f,b,g,d) ~= 0 & u(f,b,g,d) lesspoll m)) \
+\ | (EX b<a. f`b ~= 0 & (ALL g<a. ALL d<a. u(f,b,g,d) ~= 0 --> \
\ u(f,b,g,d) eqpoll m))";
by (Asm_simp_tac 1);
by (blast_tac (claset() delrules [equalityI]) 1);