src/HOL/Complex/NSComplex.thy
changeset 14320 fb7a114826be
parent 14318 7dbd3988b15b
child 14323 27724f528f82
     1.1 --- a/src/HOL/Complex/NSComplex.thy	Tue Dec 23 14:45:23 2003 +0100
     1.2 +++ b/src/HOL/Complex/NSComplex.thy	Tue Dec 23 14:45:47 2003 +0100
     1.3 @@ -1761,13 +1761,13 @@
     1.4  done
     1.5  declare hcomplex_of_complex_minus [simp]
     1.6  
     1.7 -lemma hcomplex_of_complex_one:
     1.8 +lemma hcomplex_of_complex_one [simp]:
     1.9        "hcomplex_of_complex 1 = 1"
    1.10  apply (unfold hcomplex_of_complex_def hcomplex_one_def)
    1.11  apply auto
    1.12  done
    1.13  
    1.14 -lemma hcomplex_of_complex_zero:
    1.15 +lemma hcomplex_of_complex_zero [simp]:
    1.16        "hcomplex_of_complex 0 = 0"
    1.17  apply (unfold hcomplex_of_complex_def hcomplex_zero_def)
    1.18  apply (simp (no_asm))