# HG changeset patch
# User nipkow
# Date 943269027 -3600
# Node ID 199721f2eb2d3d770d55a3495a78c603b4b24cb8
# Parent  3e5ddca613dd19395f1e71a974203e3aa6f8d782
Added linord_less_split

diff -r 3e5ddca613dd -r 199721f2eb2d src/HOL/Ord.ML
--- a/src/HOL/Ord.ML	Fri Nov 19 16:30:52 1999 +0100
+++ b/src/HOL/Ord.ML	Mon Nov 22 12:10:27 1999 +0100
@@ -116,6 +116,12 @@
 by (Blast_tac 1);
 qed "linorder_less_linear";
 
+val prems = goal thy
+ "[| (x::'a::linorder)<y ==> P; x=y ==> P; y<x ==> P |] ==> P";
+by(cut_facts_tac [linorder_less_linear] 1);
+by(REPEAT(eresolve_tac (prems@[disjE]) 1));
+qed "linorder_less_split";
+
 Goal "!!x::'a::linorder. (~ x < y) = (y <= x)";
 by (simp_tac (simpset() addsimps [order_less_le]) 1);
 by (cut_facts_tac [linorder_linear] 1);