# HG changeset patch
# User immler
# Date 1566937881 -7200
# Node ID 6bc397bc8e8a780c51d24d552196f4095112e334
# Parent  60483d0385d610e770aa33bedf4d54d0aa76c0ca
explicit instance real::ordered_real_vector before subclass in ordered_euclidean_space

diff -r 60483d0385d6 -r 6bc397bc8e8a src/HOL/Real_Vector_Spaces.thy
--- a/src/HOL/Real_Vector_Spaces.thy	Tue Aug 27 19:22:57 2019 +0200
+++ b/src/HOL/Real_Vector_Spaces.thy	Tue Aug 27 22:31:21 2019 +0200
@@ -1213,6 +1213,9 @@
 lemmas closed_real_atLeast = closed_atLeast[where 'a=real]
 lemmas closed_real_atLeastAtMost = closed_atLeastAtMost[where 'a=real]
 
+instance real :: ordered_real_vector
+  by standard (auto intro: mult_left_mono mult_right_mono)
+
 
 subsection \<open>Extra type constraints\<close>