Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/ZF/Resid/Confluence.thy
changeset 76217 8655344f1cf6
parent 76216 9fc34f76b4e8 
--- a/src/ZF/Resid/Confluence.thy	Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/Resid/Confluence.thy	Tue Sep 27 18:02:34 2022 +0100
@@ -22,7 +22,7 @@
 
 lemma strip_lemma_r: 
     "\<lbrakk>confluence(Spar_red1)\<rbrakk>\<Longrightarrow> strip"
-apply (unfold confluence_def strip_def)
+  unfolding confluence_def strip_def
 apply (rule impI [THEN allI, THEN allI])
 apply (erule Spar_red.induct, fast)
 apply (fast intro: Spar_red.trans)
@@ -31,7 +31,7 @@
 
 lemma strip_lemma_l: 
     "strip\<Longrightarrow> confluence(Spar_red)"
-apply (unfold confluence_def strip_def)
+  unfolding confluence_def strip_def
 apply (rule impI [THEN allI, THEN allI])
 apply (erule Spar_red.induct, blast)
 apply clarify
isabelle