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/HOL/Equiv_Relations.thy
changeset 25482 4ed49eccb1eb
parent 24728 e2b3a1065676
child 26791 3581a9c71909 
--- a/src/HOL/Equiv_Relations.thy	Wed Nov 28 09:01:34 2007 +0100
+++ b/src/HOL/Equiv_Relations.thy	Wed Nov 28 09:01:37 2007 +0100
@@ -288,7 +288,7 @@
    apply (rule commute [THEN trans])
      apply (rule_tac [3] commute [THEN trans, symmetric])
        apply (rule_tac [5] sym)
-       apply (assumption | rule congt |
+       apply (rule congt | assumption |
          erule equivA [THEN equiv_type, THEN subsetD, THEN SigmaE2])+
   done
isabelle