--- a/src/ZF/Resid/Residuals.thy Tue Sep 27 16:51:35 2022 +0100
+++ b/src/ZF/Resid/Residuals.thy Tue Sep 27 17:03:23 2022 +0100
@@ -199,8 +199,8 @@
subsection\<open>paving theorem\<close>
lemma paving: "\<lbrakk>w \<sim> u; w \<sim> v; regular(u); regular(v)\<rbrakk>\<Longrightarrow>
- \<exists>uv vu. (w|>u) |> vu = (w|>v) |> uv & (w|>u) \<sim> vu \<and>
- regular(vu) & (w|>v) \<sim> uv \<and> regular(uv)"
+ \<exists>uv vu. (w|>u) |> vu = (w|>v) |> uv \<and> (w|>u) \<sim> vu \<and>
+ regular(vu) \<and> (w|>v) \<sim> uv \<and> regular(uv)"
apply (subgoal_tac "u \<sim> v")
apply (safe intro!: exI)
apply (rule cube)