# HG changeset patch
# User huffman
# Date 1235492414 28800
# Node ID 4cf42465b3daefdbb4cc8eebee52ec7b630a356c
# Parent  293b896b9c25323bec3aad1ffbab1607804d6354
fix lemma hypreal_hnorm_def

diff -r 293b896b9c25 -r 4cf42465b3da 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: