1.1 --- a/src/HOL/Ord.ML	Fri Nov 19 16:30:52 1999 +0100
     1.2 +++ b/src/HOL/Ord.ML	Mon Nov 22 12:10:27 1999 +0100
     1.3 @@ -116,6 +116,12 @@
     1.4  by (Blast_tac 1);
     1.5  qed "linorder_less_linear";
     1.6  
     1.7 +val prems = goal thy
     1.8 + "[| (x::'a::linorder)<y ==> P; x=y ==> P; y<x ==> P |] ==> P";
     1.9 +by(cut_facts_tac [linorder_less_linear] 1);
    1.10 +by(REPEAT(eresolve_tac (prems@[disjE]) 1));
    1.11 +qed "linorder_less_split";
    1.12 +
    1.13  Goal "!!x::'a::linorder. (~ x < y) = (y <= x)";
    1.14  by (simp_tac (simpset() addsimps [order_less_le]) 1);
    1.15  by (cut_facts_tac [linorder_linear] 1);