src/ZF/equalities.thy

--- a/src/ZF/equalities.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/equalities.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -621,7 +621,7 @@
 (** Range **)
 
 lemma rangeI [intro]: "\<langle>a,b\<rangle>\<in> r \<Longrightarrow> b \<in> range(r)"
-apply (unfold range_def)
+  unfolding range_def
 apply (erule converseI [THEN domainI])
 done
 
@@ -629,7 +629,7 @@
 by (unfold range_def, blast)
 
 lemma range_subset: "range(A*B) \<subseteq> B"
-apply (unfold range_def)
+  unfolding range_def
 apply (subst converse_prod)
 apply (rule domain_subset)
 done
@@ -682,12 +682,12 @@
 by blast
 
 lemma domain_subset_field: "domain(r) \<subseteq> field(r)"
-apply (unfold field_def)
+  unfolding field_def
 apply (rule Un_upper1)
 done
 
 lemma range_subset_field: "range(r) \<subseteq> field(r)"
-apply (unfold field_def)
+  unfolding field_def
 apply (rule Un_upper2)
 done
 
@@ -807,7 +807,7 @@
 done
 
 lemma vimage_subset: "r \<subseteq> A*B \<Longrightarrow> r-``C \<subseteq> A"
-apply (unfold vimage_def)
+  unfolding vimage_def
 apply (erule converse_type [THEN image_subset])
 done