src/HOL/Hyperreal/NSA.ML

 (*----------------------------------------------------------------------
                    Infinitely close relation @=
  ----------------------------------------------------------------------*)
 
 Goalw [Infinitesimal_def,approx_def] 
-        "x:Infinitesimal = (x @= #0)";
+        "(x:Infinitesimal) = (x @= #0)";
 by (Simp_tac 1);
 qed "mem_infmal_iff";
 
 Goalw [approx_def]" (x @= y) = (x + -y @= #0)";
 by (Simp_tac 1);