# HG changeset patch
# User huffman
# Date 1180318964 -7200
# Node ID d5cdaa3b7517af5736e74dc1564b9a4316f6dbda
# Parent  2bc882fbe51c0ce1c00bf5a83a04e9dd56bdac58
interpretations additive_scaleR_left, additive_scaleR_right

diff -r 2bc882fbe51c -r d5cdaa3b7517 src/HOL/Real/RealVector.thy
--- a/src/HOL/Real/RealVector.thy	Mon May 28 03:45:41 2007 +0200
+++ b/src/HOL/Real/RealVector.thy	Mon May 28 04:22:44 2007 +0200
@@ -91,29 +91,25 @@
   shows "scaleR a (scaleR b x) = scaleR b (scaleR a x)"
 by (simp add: mult_commute)
 
-lemma additive_scaleR_right: "additive (\<lambda>x. scaleR a x::'a::real_vector)"
-by (rule additive.intro, rule scaleR_right_distrib)
-
-lemma additive_scaleR_left: "additive (\<lambda>a. scaleR a x::'a::real_vector)"
+interpretation additive_scaleR_left:
+  additive ["(\<lambda>a. scaleR a x::'a::real_vector)"]
 by (rule additive.intro, rule scaleR_left_distrib)
 
-lemmas scaleR_zero_left [simp] =
-  additive.zero [OF additive_scaleR_left, standard]
+interpretation additive_scaleR_right:
+  additive ["(\<lambda>x. scaleR a x::'a::real_vector)"]
+by (rule additive.intro, rule scaleR_right_distrib)
 
-lemmas scaleR_zero_right [simp] =
-  additive.zero [OF additive_scaleR_right, standard]
+lemmas scaleR_zero_left [simp] = additive_scaleR_left.zero
 
-lemmas scaleR_minus_left [simp] =
-  additive.minus [OF additive_scaleR_left, standard]
+lemmas scaleR_zero_right [simp] = additive_scaleR_right.zero
 
-lemmas scaleR_minus_right [simp] =
-  additive.minus [OF additive_scaleR_right, standard]
+lemmas scaleR_minus_left [simp] = additive_scaleR_left.minus
+
+lemmas scaleR_minus_right [simp] = additive_scaleR_right.minus
 
-lemmas scaleR_left_diff_distrib =
-  additive.diff [OF additive_scaleR_left, standard]
+lemmas scaleR_left_diff_distrib = additive_scaleR_left.diff
 
-lemmas scaleR_right_diff_distrib =
-  additive.diff [OF additive_scaleR_right, standard]
+lemmas scaleR_right_diff_distrib = additive_scaleR_right.diff
 
 lemma scaleR_eq_0_iff [simp]:
   fixes x :: "'a::real_vector"