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.
real_norm_def [simp]
authorhuffman
Sun, 24 Sep 2006 07:14:02 +0200
changeset 20694 76c49548d14c
parent 20693 f763367e332f
child 20695 1cc6fefbff1a
real_norm_def [simp]
src/HOL/Real/RealVector.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Real/RealVector.thy	Sun Sep 24 06:54:39 2006 +0200
+++ b/src/HOL/Real/RealVector.thy	Sun Sep 24 07:14:02 2006 +0200
@@ -342,7 +342,7 @@
 instance real :: norm ..
 
 defs (overloaded)
-  real_norm_def: "norm r \<equiv> \<bar>r\<bar>"
+  real_norm_def [simp]: "norm r \<equiv> \<bar>r\<bar>"
 
 axclass normed < plus, zero, norm
   norm_ge_zero [simp]: "0 \<le> norm x"
isabelle