# HG changeset patch
# User haftmann
# Date 1213988421 -7200
# Node ID 3447cd2e18e88de0c3a9b0e35bfdc2a6e6842082
# Parent  a5373b60e66c714747abfb73f6806e27d48675f8
streamlined definitions

diff -r a5373b60e66c -r 3447cd2e18e8 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Fri Jun 20 21:00:16 2008 +0200
+++ b/src/HOL/Orderings.thy	Fri Jun 20 21:00:21 2008 +0200
@@ -105,7 +105,7 @@
 
 text {* Least value operator *}
 
-definition
+definition (in ord)
   Least :: "('a \<Rightarrow> bool) \<Rightarrow> 'a" (binder "LEAST " 10) where
   "Least P = (THE x. P x \<and> (\<forall>y. P y \<longrightarrow> x \<le> y))"
 
@@ -186,7 +186,6 @@
 lemma antisym_conv3: "\<not> y < x \<Longrightarrow> \<not> x < y \<longleftrightarrow> x = y"
 by (blast intro: antisym dest: not_less [THEN iffD1])
 
-text{*Replacing the old Nat.leI*}
 lemma leI: "\<not> x < y \<Longrightarrow> y \<le> x"
 unfolding not_less .
 
@@ -208,14 +207,10 @@
 
 text {* min/max *}
 
-text {* for historic reasons, definitions are done in context ord *}
-
-definition (in ord)
-  min :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
+definition (in ord) min :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
   [code unfold, code inline del]: "min a b = (if a \<le> b then a else b)"
 
-definition (in ord)
-  max :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
+definition (in ord) max :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
   [code unfold, code inline del]: "max a b = (if a \<le> b then b else a)"
 
 lemma min_le_iff_disj: