Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix lemma hypreal_hnorm_def
authorhuffman
Tue, 24 Feb 2009 08:20:14 -0800
changeset 30080 4cf42465b3da
parent 30079 293b896b9c25
child 30081 46b9c8ae3897
child 30149 6b7ad52c5770
fix lemma hypreal_hnorm_def
src/HOL/NSA/NSA.thy file | annotate | diff | comparison | revisions 
--- 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:
isabelle