--- a/src/HOL/Orderings.thy Fri Mar 09 08:45:53 2007 +0100
+++ b/src/HOL/Orderings.thy Fri Mar 09 08:45:55 2007 +0100
@@ -228,7 +228,7 @@
lemma not_leE: "\<not> y \<sqsubseteq> x \<Longrightarrow> x \<sqsubset> y"
unfolding not_le .
-(* min/max *)
+text {* min/max *}
definition
min :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
@@ -822,6 +822,7 @@
"True < b \<longleftrightarrow> False"
unfolding le_bool_def less_bool_def by simp_all
+
subsection {* Monotonicity, syntactic least value operator and min/max *}
locale mono =