# HG changeset patch
# User huffman
# Date 1188768981 -7200
# Node ID 40b22040325702f2ab51c68bbf38623fbe18373e
# Parent  5c435b2ea13760f5411815f0d4cae9999d994fd5
fix sgn_div_norm class

diff -r 5c435b2ea137 -r 40b220403257 src/HOL/Complex/Complex.thy
--- a/src/HOL/Complex/Complex.thy	Sun Sep 02 12:34:20 2007 +0200
+++ b/src/HOL/Complex/Complex.thy	Sun Sep 02 23:36:21 2007 +0200
@@ -324,7 +324,7 @@
     by (induct x, induct y)
        (simp add: real_sqrt_mult [symmetric] power2_eq_square ring_simps)
   show "sgn x = x /\<^sub>R cmod x" by(simp add: complex_sgn_def)
-qed (* FIXME junk *) (rule refl)+
+qed
 
 lemma cmod_unit_one [simp]: "cmod (Complex (cos a) (sin a)) = 1"
 by simp
diff -r 5c435b2ea137 -r 40b220403257 src/HOL/Real/RealVector.thy
--- a/src/HOL/Real/RealVector.thy	Sun Sep 02 12:34:20 2007 +0200
+++ b/src/HOL/Real/RealVector.thy	Sun Sep 02 23:36:21 2007 +0200
@@ -377,12 +377,8 @@
 instance real :: norm
   real_norm_def [simp]: "norm r \<equiv> \<bar>r\<bar>" ..
 
-class sgn_div_norm = scaleR + inverse + norm + sgn +
-assumes sgn_div_norm: "sgn x = x /# norm x"
-(* FIXME junk needed because of broken locale interpretation *)
-and "(sgn :: 'a::scaleR \<Rightarrow> 'a) = sgn"
-and "(inverse :: 'a::scaleR \<Rightarrow> 'a) = inverse"
-and "(scaleR :: real \<Rightarrow> 'a::scaleR \<Rightarrow> 'a) = scaleR"
+class sgn_div_norm = scaleR + norm + sgn +
+  assumes sgn_div_norm: "sgn x = x /# norm x"
 
 axclass real_normed_vector < real_vector, sgn_div_norm
   norm_ge_zero [simp]: "0 \<le> norm x"
@@ -415,8 +411,6 @@
 instance real :: real_normed_field
 apply (intro_classes, unfold real_norm_def real_scaleR_def)
 apply (simp add: real_sgn_def)
-(* FIXME junk *)
-apply(rule refl)+
 apply (rule abs_ge_zero)
 apply (rule abs_eq_0)
 apply (rule abs_triangle_ineq)