# HG changeset patch
# User huffman
# Date 1180455596 -7200
# Node ID a34f204e9c883469e95bee5d3e811adf9a1534bf
# Parent  0082459a255b50adb13071c90f5d0502c296d00e
interpretation bounded_linear_divide

diff -r 0082459a255b -r a34f204e9c88 src/HOL/Real/RealVector.thy
--- a/src/HOL/Real/RealVector.thy	Tue May 29 17:37:04 2007 +0200
+++ b/src/HOL/Real/RealVector.thy	Tue May 29 18:19:56 2007 +0200
@@ -756,6 +756,11 @@
   bounded_linear ["(\<lambda>y::'a::real_normed_algebra. x * y)"]
 by (rule bounded_bilinear_mult.bounded_linear_right)
 
+interpretation bounded_linear_divide:
+  bounded_linear ["(\<lambda>x::'a::real_normed_field. x / y)"]
+unfolding divide_inverse
+by (rule bounded_bilinear_mult.bounded_linear_left)
+
 interpretation bounded_bilinear_scaleR:
   bounded_bilinear ["scaleR"]
 apply (rule bounded_bilinear.intro)