--- a/src/HOL/Complex.thy Thu May 28 17:24:18 2009 -0700
+++ b/src/HOL/Complex.thy Thu May 28 22:53:23 2009 -0700
@@ -278,6 +278,9 @@
definition
complex_sgn_def: "sgn x = x /\<^sub>R cmod x"
+definition
+ dist_complex_def: "dist x y = cmod (x - y)"
+
lemmas cmod_def = complex_norm_def
lemma complex_norm [simp]: "cmod (Complex x y) = sqrt (x\<twosuperior> + y\<twosuperior>)"
@@ -299,7 +302,10 @@
show "norm (x * y) = norm x * norm y"
by (induct x, induct y)
(simp add: real_sqrt_mult [symmetric] power2_eq_square algebra_simps)
- show "sgn x = x /\<^sub>R cmod x" by(simp add: complex_sgn_def)
+ show "sgn x = x /\<^sub>R cmod x"
+ by (rule complex_sgn_def)
+ show "dist x y = cmod (x - y)"
+ by (rule dist_complex_def)
qed
end