src/HOL/Analysis/Conformal_Mappings.thy
changeset 70347 e5cd5471c18a
parent 70346 408e15cbd2a6
child 70365 4df0628e8545
     1.1 --- a/src/HOL/Analysis/Conformal_Mappings.thy	Fri Jun 14 08:34:28 2019 +0000
     1.2 +++ b/src/HOL/Analysis/Conformal_Mappings.thy	Fri Jun 14 08:34:28 2019 +0000
     1.3 @@ -1878,9 +1878,9 @@
     1.4          apply (simp add: power2_eq_square divide_simps C_def norm_mult)
     1.5          proof -
     1.6            have "norm z * (norm (deriv f 0) * (r - norm z - norm z)) \<le> norm z * (norm (deriv f 0) * (r - norm z) - norm (deriv f 0) * norm z)"
     1.7 -            by (simp add: sign_simps)
     1.8 +            by (simp add: algebra_simps)
     1.9            then show "(norm z * (r - norm z) - norm z * norm z) * norm (deriv f 0) \<le> norm (deriv f 0) * norm z * (r - norm z) - norm z * norm z * norm (deriv f 0)"
    1.10 -            by (simp add: sign_simps)
    1.11 +            by (simp add: algebra_simps)
    1.12          qed
    1.13      qed
    1.14      have sq201 [simp]: "0 < (1 - sqrt 2 / 2)" "(1 - sqrt 2 / 2)  < 1"