explicit instance real::ordered_real_vector before subclass in ordered_euclidean_space
authorimmler
Tue, 27 Aug 2019 22:31:21 +0200
changeset 70803 6bc397bc8e8a
parent 70802 60483d0385d6
child 70804 c81ac117afa6
explicit instance real::ordered_real_vector before subclass in ordered_euclidean_space
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>