1.1 --- a/src/HOL/Complex.thy	Tue Nov 19 01:30:14 2013 +0100
     1.2 +++ b/src/HOL/Complex.thy	Tue Nov 19 10:05:53 2013 +0100
     1.3 @@ -108,7 +108,12 @@
     1.4  definition complex_divide_def:
     1.5    "x / (y\<Colon>complex) = x * inverse y"
     1.6  
     1.7 -lemma Complex_eq_1 [simp]: "(Complex a b = 1) = (a = 1 \<and> b = 0)"
     1.8 +lemma Complex_eq_1 [simp]:
     1.9 +  "Complex a b = 1 \<longleftrightarrow> a = 1 \<and> b = 0"
    1.10 +  by (simp add: complex_one_def)
    1.11 +
    1.12 +lemma Complex_eq_neg_1 [simp]:
    1.13 +  "Complex a b = - 1 \<longleftrightarrow> a = - 1 \<and> b = 0"
    1.14    by (simp add: complex_one_def)
    1.15  
    1.16  lemma complex_Re_one [simp]: "Re 1 = 1"
    1.17 @@ -166,21 +171,21 @@
    1.18  lemma complex_Re_numeral [simp]: "Re (numeral v) = numeral v"
    1.19    using complex_Re_of_int [of "numeral v"] by simp
    1.20  
    1.21 -lemma complex_Re_neg_numeral [simp]: "Re (neg_numeral v) = neg_numeral v"
    1.22 -  using complex_Re_of_int [of "neg_numeral v"] by simp
    1.23 +lemma complex_Re_neg_numeral [simp]: "Re (- numeral v) = - numeral v"
    1.24 +  using complex_Re_of_int [of "- numeral v"] by simp
    1.25  
    1.26  lemma complex_Im_numeral [simp]: "Im (numeral v) = 0"
    1.27    using complex_Im_of_int [of "numeral v"] by simp
    1.28  
    1.29 -lemma complex_Im_neg_numeral [simp]: "Im (neg_numeral v) = 0"
    1.30 -  using complex_Im_of_int [of "neg_numeral v"] by simp
    1.31 +lemma complex_Im_neg_numeral [simp]: "Im (- numeral v) = 0"
    1.32 +  using complex_Im_of_int [of "- numeral v"] by simp
    1.33  
    1.34  lemma Complex_eq_numeral [simp]:
    1.35 -  "(Complex a b = numeral w) = (a = numeral w \<and> b = 0)"
    1.36 +  "Complex a b = numeral w \<longleftrightarrow> a = numeral w \<and> b = 0"
    1.37    by (simp add: complex_eq_iff)
    1.38  
    1.39  lemma Complex_eq_neg_numeral [simp]:
    1.40 -  "(Complex a b = neg_numeral w) = (a = neg_numeral w \<and> b = 0)"
    1.41 +  "Complex a b = - numeral w \<longleftrightarrow> a = - numeral w \<and> b = 0"
    1.42    by (simp add: complex_eq_iff)
    1.43  
    1.44  
    1.45 @@ -421,7 +426,7 @@
    1.46  lemma complex_i_not_numeral [simp]: "ii \<noteq> numeral w"
    1.47    by (simp add: complex_eq_iff)
    1.48  
    1.49 -lemma complex_i_not_neg_numeral [simp]: "ii \<noteq> neg_numeral w"
    1.50 +lemma complex_i_not_neg_numeral [simp]: "ii \<noteq> - numeral w"
    1.51    by (simp add: complex_eq_iff)
    1.52  
    1.53  lemma i_mult_Complex [simp]: "ii * Complex a b = Complex (- b) a"
    1.54 @@ -508,7 +513,7 @@
    1.55  lemma complex_cnj_numeral [simp]: "cnj (numeral w) = numeral w"
    1.56    by (simp add: complex_eq_iff)
    1.57  
    1.58 -lemma complex_cnj_neg_numeral [simp]: "cnj (neg_numeral w) = neg_numeral w"
    1.59 +lemma complex_cnj_neg_numeral [simp]: "cnj (- numeral w) = - numeral w"
    1.60    by (simp add: complex_eq_iff)
    1.61  
    1.62  lemma complex_cnj_scaleR: "cnj (scaleR r x) = scaleR r (cnj x)"