src/HOL/Equiv_Relations.thy
changeset 35216 7641e8d831d2
parent 30198 922f944f03b2
child 35725 4d7e3cc9c52c
     1.1 --- a/src/HOL/Equiv_Relations.thy	Thu Feb 18 13:29:59 2010 -0800
     1.2 +++ b/src/HOL/Equiv_Relations.thy	Thu Feb 18 14:21:44 2010 -0800
     1.3 @@ -328,7 +328,7 @@
     1.4     apply assumption
     1.5    apply simp
     1.6   apply(fastsimp simp add:inj_on_def)
     1.7 -apply (simp add:setsum_constant)
     1.8 +apply simp
     1.9  done
    1.10  
    1.11  end