--- 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);