diff -r 19cc354ba625 -r c40bdfc84640 src/HOL/Induct/QuoNestedDataType.thy
--- a/src/HOL/Induct/QuoNestedDataType.thy	Thu Mar 28 08:30:42 2024 +0100
+++ b/src/HOL/Induct/QuoNestedDataType.thy	Wed Mar 27 18:29:32 2024 +0100
@@ -49,11 +49,10 @@
     (blast intro: exprel.intros listrel.intros)+
 
 theorem equiv_exprel: "equiv UNIV exprel"
-proof -
-  have "refl exprel" by (simp add: refl_on_def exprel_refl)
-  moreover have "sym exprel" by (simp add: sym_def, blast intro: exprel.SYM)
-  moreover have "trans exprel" by (simp add: trans_def, blast intro: exprel.TRANS)
-  ultimately show ?thesis by (simp add: equiv_def)
+proof (rule equivI)
+  show "refl exprel" by (simp add: refl_on_def exprel_refl)
+  show "sym exprel" by (simp add: sym_def, blast intro: exprel.SYM)
+  show "trans exprel" by (simp add: trans_def, blast intro: exprel.TRANS)
 qed
 
 theorem equiv_list_exprel: "equiv UNIV (listrel exprel)"