src/HOL/Equiv_Relations.thy
changeset 25482 4ed49eccb1eb
parent 24728 e2b3a1065676
child 26791 3581a9c71909
     1.1 --- a/src/HOL/Equiv_Relations.thy	Wed Nov 28 09:01:34 2007 +0100
     1.2 +++ b/src/HOL/Equiv_Relations.thy	Wed Nov 28 09:01:37 2007 +0100
     1.3 @@ -288,7 +288,7 @@
     1.4     apply (rule commute [THEN trans])
     1.5       apply (rule_tac [3] commute [THEN trans, symmetric])
     1.6         apply (rule_tac [5] sym)
     1.7 -       apply (assumption | rule congt |
     1.8 +       apply (rule congt | assumption |
     1.9           erule equivA [THEN equiv_type, THEN subsetD, THEN SigmaE2])+
    1.10    done
    1.11