src/HOL/NthRoot.thy
changeset 56536 aefb4a8da31f
parent 56381 0556204bc230
child 56889 48a745e1bde7
     1.1 --- a/src/HOL/NthRoot.thy	Fri Apr 11 12:43:22 2014 +0200
     1.2 +++ b/src/HOL/NthRoot.thy	Fri Apr 11 13:36:57 2014 +0200
     1.3 @@ -602,7 +602,7 @@
     1.4  apply (rule_tac b="(a * d - b * c)\<^sup>2" in ord_le_eq_trans)
     1.5  apply (rule zero_le_power2)
     1.6  apply (simp add: power2_diff power_mult_distrib)
     1.7 -apply (simp add: mult_nonneg_nonneg)
     1.8 +apply (simp)
     1.9  apply simp
    1.10  apply (simp add: add_increasing)
    1.11  done