# HG changeset patch
# User nipkow
# Date 962705056 -7200
# Node ID c472ed4edded6de2fb234bc032326a652385fc42
# Parent  f961c1fdff505ca7e62d04b7756b6aa3adb10764
added a thm.

diff -r f961c1fdff50 -r c472ed4edded src/HOL/Ord.ML
--- a/src/HOL/Ord.ML	Tue Jul 04 10:54:46 2000 +0200
+++ b/src/HOL/Ord.ML	Tue Jul 04 12:04:16 2000 +0200
@@ -214,6 +214,12 @@
 by (blast_tac (claset() addIs [order_trans]) 1);
 qed "min_le_iff_disj";
 
+Goalw [min_def] "!!z::'a::linorder. (min x y < z) = (x < z | y < z)";
+by (simp_tac (simpset() addsimps [order_le_less]) 1);
+by (cut_facts_tac [linorder_less_linear] 1);
+by (blast_tac (claset() addIs [order_less_trans]) 1);
+qed "min_less_iff_disj";
+
 Goalw [min_def]
  "P(min (i::'a::linorder) j) = ((i <= j --> P(i)) & (~ i <= j --> P(j)))";
 by (Simp_tac 1);