diff -r 1a20fd9cf281 -r eb4ddd18d635 src/HOL/Complex.thy --- a/src/HOL/Complex.thy Sun Apr 24 21:31:14 2016 +0200 +++ b/src/HOL/Complex.thy Mon Apr 25 16:09:26 2016 +0200 @@ -817,7 +817,8 @@ from assms have "z \ 0" by auto have "(SOME a. sgn z = cis a \ -pi < a \ a \ pi) = x" proof - fix a def d \ "a - x" + fix a + define d where "d = a - x" assume a: "sgn z = cis a \ - pi < a \ a \ pi" from a assms have "- (2*pi) < d \ d < 2*pi" unfolding d_def by simp @@ -839,7 +840,7 @@ proof (simp add: arg_def assms, rule someI_ex) obtain r a where z: "z = rcis r a" using rcis_Ex by fast with assms have "r \ 0" by auto - def b \ "if 0 < r then a else a + pi" + define b where "b = (if 0 < r then a else a + pi)" have b: "sgn z = cis b" unfolding z b_def rcis_def using \r \ 0\ by (simp add: of_real_def sgn_scaleR sgn_if complex_eq_iff) @@ -848,7 +849,7 @@ have cis_2pi_int: "\x. cis (2 * pi * real_of_int x) = 1" by (case_tac x rule: int_diff_cases) (simp add: right_diff_distrib cis_divide [symmetric] cis_2pi_nat) - def c \ "b - 2*pi * of_int \(b - pi) / (2*pi)\" + define c where "c = b - 2 * pi * of_int \(b - pi) / (2 * pi)\" have "sgn z = cis c" unfolding b c_def by (simp add: cis_divide [symmetric] cis_2pi_int)