src/HOL/Complex/ex/BinEx.thy
changeset 14373 67a628beb981
parent 14051 4b61bbb0dcab
child 15149 c5c4884634b7
     1.1 --- a/src/HOL/Complex/ex/BinEx.thy	Tue Feb 03 10:19:21 2004 +0100
     1.2 +++ b/src/HOL/Complex/ex/BinEx.thy	Tue Feb 03 11:06:36 2004 +0100
     1.3 @@ -381,8 +381,7 @@
     1.4  text{*Multiplication requires distributive laws.  Perhaps versions instantiated
     1.5  to literal constants should be added to the simpset.*}
     1.6  
     1.7 -lemmas distrib = complex_add_mult_distrib complex_add_mult_distrib2
     1.8 -                 complex_diff_mult_distrib complex_diff_mult_distrib2
     1.9 +lemmas distrib = left_distrib right_distrib left_diff_distrib right_diff_distrib
    1.10  
    1.11  lemma "(1 + ii) * (1 - ii) = 2"
    1.12  by (simp add: distrib)
    1.13 @@ -393,10 +392,8 @@
    1.14  lemma "(-84 + 255*ii) + (51 * 255*ii) = -84 + 13260 * ii"
    1.15  by (simp add: distrib)
    1.16  
    1.17 -text{*No inequalities: we have no ordering on the complex numbers.*}
    1.18 +text{*No inequalities or linear arithmetic: the complex numbers are unordered!*}
    1.19  
    1.20  text{*No powers (not supported yet)*}
    1.21  
    1.22 -text{*No linear arithmetic*}
    1.23 -
    1.24  end