src/HOL/Equiv_Relations.thy
changeset 15539 333a88244569
parent 15392 290bc97038c7
child 17589 58eeffd73be1
     1.1 --- a/src/HOL/Equiv_Relations.thy	Sat Feb 19 18:44:34 2005 +0100
     1.2 +++ b/src/HOL/Equiv_Relations.thy	Mon Feb 21 15:04:10 2005 +0100
     1.3 @@ -327,7 +327,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_nat)
     1.8 +apply (simp add:setsum_constant)
     1.9  done
    1.10  
    1.11  ML