src/HOL/NthRoot.thy
changeset 49962 a8cc904a6820
parent 49753 a344f1a21211
child 51478 270b21f3ae0a
     1.1 --- a/src/HOL/NthRoot.thy	Fri Oct 19 10:46:42 2012 +0200
     1.2 +++ b/src/HOL/NthRoot.thy	Fri Oct 19 15:12:52 2012 +0200
     1.3 @@ -598,7 +598,7 @@
     1.4    "sqrt ((a + c)\<twosuperior> + (b + d)\<twosuperior>) \<le> sqrt (a\<twosuperior> + b\<twosuperior>) + sqrt (c\<twosuperior> + d\<twosuperior>)"
     1.5  apply (rule power2_le_imp_le, simp)
     1.6  apply (simp add: power2_sum)
     1.7 -apply (simp only: mult_assoc right_distrib [symmetric])
     1.8 +apply (simp only: mult_assoc distrib_left [symmetric])
     1.9  apply (rule mult_left_mono)
    1.10  apply (rule power2_le_imp_le)
    1.11  apply (simp add: power2_sum power_mult_distrib)