src/HOL/Complex.thy
changeset 29667 53103fc8ffa3
parent 29233 ce6d35a0bed6
child 30273 ecd6f0ca62ea
     1.1 --- a/src/HOL/Complex.thy	Sun Jan 18 13:58:17 2009 +0100
     1.2 +++ b/src/HOL/Complex.thy	Wed Jan 28 16:29:16 2009 +0100
     1.3 @@ -237,9 +237,9 @@
     1.4    show "scaleR 1 x = x"
     1.5      by (simp add: expand_complex_eq)
     1.6    show "scaleR a x * y = scaleR a (x * y)"
     1.7 -    by (simp add: expand_complex_eq ring_simps)
     1.8 +    by (simp add: expand_complex_eq algebra_simps)
     1.9    show "x * scaleR a y = scaleR a (x * y)"
    1.10 -    by (simp add: expand_complex_eq ring_simps)
    1.11 +    by (simp add: expand_complex_eq algebra_simps)
    1.12  qed
    1.13  
    1.14  end
    1.15 @@ -312,7 +312,7 @@
    1.16         (simp add: power_mult_distrib right_distrib [symmetric] real_sqrt_mult)
    1.17    show "norm (x * y) = norm x * norm y"
    1.18      by (induct x, induct y)
    1.19 -       (simp add: real_sqrt_mult [symmetric] power2_eq_square ring_simps)
    1.20 +       (simp add: real_sqrt_mult [symmetric] power2_eq_square algebra_simps)
    1.21    show "sgn x = x /\<^sub>R cmod x" by(simp add: complex_sgn_def)
    1.22  qed
    1.23