src/HOL/Complex/NSComplexBin.ML
changeset 14378 69c4d5997669
parent 14377 f454b3004f8f
     1.1 --- a/src/HOL/Complex/NSComplexBin.ML	Thu Feb 05 10:45:28 2004 +0100
     1.2 +++ b/src/HOL/Complex/NSComplexBin.ML	Tue Feb 10 12:02:11 2004 +0100
     1.3 @@ -100,7 +100,7 @@
     1.4  (** Equals (=) **)
     1.5  
     1.6  Goal "((number_of v :: hcomplex) = number_of v') = \
     1.7 -\     iszero (number_of (bin_add v (bin_minus v')))";
     1.8 +\     iszero (number_of (bin_add v (bin_minus v')) :: int)";
     1.9  by (simp_tac
    1.10      (HOL_ss addsimps [hcomplex_number_of_def, 
    1.11  	              hcomplex_of_complex_eq_iff, eq_complex_number_of]) 1);