src/HOL/Complex/NSComplex.thy

 
 
 subsection{*Additive Inverse on Nonstandard Complex Numbers*}
 
 lemma hcomplex_minus_congruent:
-     "congruent hcomplexrel (%X. hcomplexrel `` {%n. - (X n)})"
+     "(%X. hcomplexrel `` {%n. - (X n)}) respects hcomplexrel"
 by (simp add: congruent_def)
 
 lemma hcomplex_minus:
   "- (Abs_hcomplex(hcomplexrel `` {%n. X n})) =
       Abs_hcomplex(hcomplexrel `` {%n. -(X n)})"