# HG changeset patch
# User nipkow
# Date 1547229926 -3600
# Node ID 7d02b7bee660bb38af33a7a52236424f8f6d6453
# Parent  6c3e6038e74cb605212ac8879f8b309fb15b86f2
tuned

diff -r 6c3e6038e74c -r 7d02b7bee660 src/HOL/Analysis/Ordered_Euclidean_Space.thy
--- a/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Fri Jan 11 18:41:50 2019 +0100
+++ b/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Fri Jan 11 19:05:26 2019 +0100
@@ -6,7 +6,7 @@
   "HOL-Library.Product_Order"
 begin
 
-subsection%important \<open>An ordering on euclidean spaces that will allow us to talk about intervals\<close>
+text%important \<open>An ordering on euclidean spaces that will allow us to talk about intervals\<close>
 
 class ordered_euclidean_space = ord + inf + sup + abs + Inf + Sup + euclidean_space +
   assumes eucl_le: "x \<le> y \<longleftrightarrow> (\<forall>i\<in>Basis. x \<bullet> i \<le> y \<bullet> i)"