src/HOL/Orderings.thy
changeset 22424 8a5412121687
parent 22384 33a46e6c7f04
child 22473 753123c89d72
     1.1 --- a/src/HOL/Orderings.thy	Fri Mar 09 08:45:53 2007 +0100
     1.2 +++ b/src/HOL/Orderings.thy	Fri Mar 09 08:45:55 2007 +0100
     1.3 @@ -228,7 +228,7 @@
     1.4  lemma not_leE: "\<not> y \<sqsubseteq> x \<Longrightarrow> x \<sqsubset> y"
     1.5    unfolding not_le .
     1.6  
     1.7 -(* min/max *)
     1.8 +text {* min/max *}
     1.9  
    1.10  definition
    1.11    min :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
    1.12 @@ -822,6 +822,7 @@
    1.13    "True < b \<longleftrightarrow> False"
    1.14    unfolding le_bool_def less_bool_def by simp_all
    1.15  
    1.16 +
    1.17  subsection {* Monotonicity, syntactic least value operator and min/max *}
    1.18  
    1.19  locale mono =