| changeset 76216 | 9fc34f76b4e8 |
| parent 76215 | a642599ffdea |
| child 76217 | 8655344f1cf6 |
--- a/src/ZF/Resid/Confluence.thy Tue Sep 27 17:46:52 2022 +0100 +++ b/src/ZF/Resid/Confluence.thy Tue Sep 27 17:54:20 2022 +0100 @@ -110,7 +110,7 @@ apply (blast intro: red1D1 redD2) apply (blast intro: red1D1 redD2) apply (cut_tac confluence_beta_reduction) -apply (unfold confluence_def) + unfolding confluence_def apply (blast intro: Sred.trans) done