--- a/src/ZF/AC/AC18_AC19.thy Mon Jan 21 10:52:05 2002 +0100
+++ b/src/ZF/AC/AC18_AC19.thy Mon Jan 21 11:25:45 2002 +0100
@@ -66,7 +66,7 @@
lemma lemma1_1: "[|c \<in> a; x = c Un {0}; x \<notin> a |] ==> x - {0} \<in> a"
apply clarify
-apply (rule subst_elem , (assumption))
+apply (rule subst_elem, assumption)
apply (fast elim: notE subst_elem)
done
@@ -98,10 +98,9 @@
apply (case_tac "A=0", force)
apply (erule_tac x = "{uu (a) . a \<in> A}" in allE)
apply (erule impE)
-apply (erule RepRep_conj , (assumption))
+apply (erule RepRep_conj, assumption)
apply (rule lemma1)
-apply (drule lemma2 , (assumption))
-apply auto
+apply (drule lemma2, assumption, auto)
done
end