--- a/src/HOL/RealVector.thy Thu Mar 26 19:24:21 2009 +0100
+++ b/src/HOL/RealVector.thy Thu Mar 26 20:08:55 2009 +0100
@@ -145,7 +145,7 @@
and scaleR_scaleR: "scaleR a (scaleR b x) = scaleR (a * b) x"
and scaleR_one: "scaleR 1 x = x"
-interpretation real_vector!:
+interpretation real_vector:
vector_space "scaleR :: real \<Rightarrow> 'a \<Rightarrow> 'a::real_vector"
apply unfold_locales
apply (rule scaleR_right_distrib)
@@ -190,10 +190,10 @@
end
-interpretation scaleR_left!: additive "(\<lambda>a. scaleR a x::'a::real_vector)"
+interpretation scaleR_left: additive "(\<lambda>a. scaleR a x::'a::real_vector)"
proof qed (rule scaleR_left_distrib)
-interpretation scaleR_right!: additive "(\<lambda>x. scaleR a x::'a::real_vector)"
+interpretation scaleR_right: additive "(\<lambda>x. scaleR a x::'a::real_vector)"
proof qed (rule scaleR_right_distrib)
lemma nonzero_inverse_scaleR_distrib:
@@ -789,7 +789,7 @@
end
-interpretation mult!:
+interpretation mult:
bounded_bilinear "op * :: 'a \<Rightarrow> 'a \<Rightarrow> 'a::real_normed_algebra"
apply (rule bounded_bilinear.intro)
apply (rule left_distrib)
@@ -800,19 +800,19 @@
apply (simp add: norm_mult_ineq)
done
-interpretation mult_left!:
+interpretation mult_left:
bounded_linear "(\<lambda>x::'a::real_normed_algebra. x * y)"
by (rule mult.bounded_linear_left)
-interpretation mult_right!:
+interpretation mult_right:
bounded_linear "(\<lambda>y::'a::real_normed_algebra. x * y)"
by (rule mult.bounded_linear_right)
-interpretation divide!:
+interpretation divide:
bounded_linear "(\<lambda>x::'a::real_normed_field. x / y)"
unfolding divide_inverse by (rule mult.bounded_linear_left)
-interpretation scaleR!: bounded_bilinear "scaleR"
+interpretation scaleR: bounded_bilinear "scaleR"
apply (rule bounded_bilinear.intro)
apply (rule scaleR_left_distrib)
apply (rule scaleR_right_distrib)
@@ -822,13 +822,13 @@
apply (simp add: norm_scaleR)
done
-interpretation scaleR_left!: bounded_linear "\<lambda>r. scaleR r x"
+interpretation scaleR_left: bounded_linear "\<lambda>r. scaleR r x"
by (rule scaleR.bounded_linear_left)
-interpretation scaleR_right!: bounded_linear "\<lambda>x. scaleR r x"
+interpretation scaleR_right: bounded_linear "\<lambda>x. scaleR r x"
by (rule scaleR.bounded_linear_right)
-interpretation of_real!: bounded_linear "\<lambda>r. of_real r"
+interpretation of_real: bounded_linear "\<lambda>r. of_real r"
unfolding of_real_def by (rule scaleR.bounded_linear_left)
end