src/ZF/AC.thy

--- a/src/ZF/AC.thy	Mon Jul 01 18:16:18 2002 +0200
+++ b/src/ZF/AC.thy	Tue Jul 02 13:28:08 2002 +0200
@@ -23,27 +23,22 @@
 (*Using dtac, this has the advantage of DELETING the universal quantifier*)
 lemma AC_ball_Pi: "\<forall>x \<in> A. \<exists>y. y \<in> B(x) ==> \<exists>y. y \<in> Pi(A,B)"
 apply (rule AC_Pi)
-apply (erule bspec)
-apply assumption
+apply (erule bspec, assumption)
 done
 
 lemma AC_Pi_Pow: "\<exists>f. f \<in> (\<Pi>X \<in> Pow(C)-{0}. X)"
 apply (rule_tac B1 = "%x. x" in AC_Pi [THEN exE])
-apply (erule_tac [2] exI)
-apply blast
+apply (erule_tac [2] exI, blast)
 done
 
 lemma AC_func:
      "[| !!x. x \<in> A ==> (\<exists>y. y \<in> x) |] ==> \<exists>f \<in> A->Union(A). \<forall>x \<in> A. f`x \<in> x"
 apply (rule_tac B1 = "%x. x" in AC_Pi [THEN exE])
-prefer 2 apply (blast dest: apply_type intro: Pi_type)
-apply (blast intro: elim:); 
+prefer 2 apply (blast dest: apply_type intro: Pi_type, blast) 
 done
 
 lemma non_empty_family: "[| 0 \<notin> A;  x \<in> A |] ==> \<exists>y. y \<in> x"
-apply (subgoal_tac "x \<noteq> 0")
-apply blast+
-done
+by (subgoal_tac "x \<noteq> 0", blast+)
 
 lemma AC_func0: "0 \<notin> A ==> \<exists>f \<in> A->Union(A). \<forall>x \<in> A. f`x \<in> x"
 apply (rule AC_func)
@@ -53,9 +48,8 @@
 lemma AC_func_Pow: "\<exists>f \<in> (Pow(C)-{0}) -> C. \<forall>x \<in> Pow(C)-{0}. f`x \<in> x"
 apply (rule AC_func0 [THEN bexE])
 apply (rule_tac [2] bexI)
-prefer 2 apply (assumption)
-apply (erule_tac [2] fun_weaken_type)
-apply blast+
+prefer 2 apply assumption
+apply (erule_tac [2] fun_weaken_type, blast+)
 done
 
 lemma AC_Pi0: "0 \<notin> A ==> \<exists>f. f \<in> (\<Pi>x \<in> A. x)"