# HG changeset patch
# User wenzelm
# Date 1002135182 -7200
# Node ID 93aaafb6431b638668fcb9cf2076831f535daad4
# Parent  b2d27a80b0d08e0420bbaa20a079bc3601d9ad92
linorder_cases supersedes linorder_less_split;
tuned parentheses in relational expressions;

diff -r b2d27a80b0d0 -r 93aaafb6431b src/HOL/Ord.thy
--- a/src/HOL/Ord.thy	Wed Oct 03 11:45:24 2001 +0200
+++ b/src/HOL/Ord.thy	Wed Oct 03 20:53:02 2001 +0200
@@ -82,7 +82,7 @@
   order_refl [iff]:                          "x <= x"
   order_trans:      "[| x <= y; y <= z |] ==> x <= z"
   order_antisym:    "[| x <= y; y <= x |] ==> x = y"
-  order_less_le:    "x < y = (x <= y & x ~= y)"
+  order_less_le:    "(x < y) = (x <= y & x ~= y)"
 
 (** Reflexivity **)
 
@@ -96,7 +96,7 @@
 apply (simp (no_asm) add: order_less_le)
 done
 
-lemma order_le_less: "(x::'a::order) <= y = (x < y | x = y)"
+lemma order_le_less: "((x::'a::order) <= y) = (x < y | x = y)"
 apply (simp (no_asm) add: order_less_le)
    (*NOT suitable for AddIffs, since it can cause PROOF FAILED*)
 apply (blast intro!: order_refl)
@@ -201,7 +201,7 @@
 apply blast
 done
 
-lemma linorder_less_split: 
+lemma linorder_cases [case_names less equal greater]:
   "[| (x::'a::linorder)<y ==> P; x=y ==> P; y<x ==> P |] ==> P"
 apply (cut_tac linorder_less_linear)
 apply blast
@@ -370,7 +370,7 @@
 val order_less_imp_not_eq = thm "order_less_imp_not_eq";
 val order_less_imp_not_eq2 = thm "order_less_imp_not_eq2";
 val linorder_less_linear = thm "linorder_less_linear";
-val linorder_less_split = thm "linorder_less_split";
+val linorder_cases = thm "linorder_cases";
 val linorder_not_less = thm "linorder_not_less";
 val linorder_not_le = thm "linorder_not_le";
 val linorder_neq_iff = thm "linorder_neq_iff";