src/ZF/EquivClass.thy

     "\<lbrakk>refl(A,r); r \<subseteq> A*A\<rbrakk> \<Longrightarrow> r \<subseteq> converse(r) O r"
 by (unfold refl_def, blast)
 
 lemma equiv_comp_eq:
     "equiv(A,r) \<Longrightarrow> converse(r) O r = r"
-apply (unfold equiv_def)
+  unfolding equiv_def
 apply (blast del: subsetI intro!: sym_trans_comp_subset refl_comp_subset)
 done
 
 (*second half*)
 lemma comp_equivI:

     "\<lbrakk>sym(r);  trans(r);  \<langle>a,b\<rangle>: r\<rbrakk> \<Longrightarrow> r``{a} \<subseteq> r``{b}"
 by (unfold trans_def sym_def, blast)
 
 lemma equiv_class_eq:
     "\<lbrakk>equiv(A,r);  \<langle>a,b\<rangle>: r\<rbrakk> \<Longrightarrow> r``{a} = r``{b}"
-apply (unfold equiv_def)
+  unfolding equiv_def
 apply (safe del: subsetI intro!: equalityI equiv_class_subset)
 apply (unfold sym_def, blast)
 done
 
 lemma equiv_class_self:

 (*** Quotients ***)
 
 (** Introduction/elimination rules -- needed? **)
 
 lemma quotientI [TC]: "x \<in> A \<Longrightarrow> r``{x}: A//r"
-apply (unfold quotient_def)
+  unfolding quotient_def
 apply (erule RepFunI)
 done
 
 lemma quotientE:
     "\<lbrakk>X \<in> A//r;  \<And>x. \<lbrakk>X = r``{x};  x \<in> A\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"

     "equiv(A,r) \<Longrightarrow> \<Union>(A//r) = A"
 by (unfold equiv_def refl_def quotient_def, blast)
 
 lemma quotient_disj:
     "\<lbrakk>equiv(A,r);  X \<in> A//r;  Y \<in> A//r\<rbrakk> \<Longrightarrow> X=Y | (X \<inter> Y \<subseteq> 0)"
-apply (unfold quotient_def)
+  unfolding quotient_def
 apply (safe intro!: equiv_class_eq, assumption)
 apply (unfold equiv_def trans_def sym_def, blast)
 done
 
 subsection\<open>Defining Unary Operations upon Equivalence Classes\<close>