src/HOL/NSA/NSA.thy

--- a/src/HOL/NSA/NSA.thy	Mon Feb 23 16:25:52 2009 -0800
+++ b/src/HOL/NSA/NSA.thy	Tue Feb 24 08:20:14 2009 -0800
@@ -157,7 +157,7 @@
 by transfer (rule norm_divide)
 
 lemma hypreal_hnorm_def [simp]:
-  "\<And>r::hypreal. hnorm r \<equiv> \<bar>r\<bar>"
+  "\<And>r::hypreal. hnorm r = \<bar>r\<bar>"
 by transfer (rule real_norm_def)
 
 lemma hnorm_add_less: