# HG changeset patch
# User huffman
# Date 1159074842 -7200
# Node ID 76c49548d14c0ed1030854bab31f767e3c046760
# Parent  f763367e332f46a460c075ed826373f131705702
real_norm_def [simp]

diff -r f763367e332f -r 76c49548d14c src/HOL/Real/RealVector.thy
--- 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"