src/HOL/HOL.thy
changeset 15079 2ef899e4526d
parent 14981 e73f8140af78
child 15103 79846e8792eb
     1.1 --- a/src/HOL/HOL.thy	Tue Jul 27 15:39:59 2004 +0200
     1.2 +++ b/src/HOL/HOL.thy	Wed Jul 28 10:49:29 2004 +0200
     1.3 @@ -818,6 +818,9 @@
     1.4    apply (insert linorder_linear, blast)
     1.5    done
     1.6  
     1.7 +lemma linorder_le_less_linear: "!!x::'a::linorder. x\<le>y | y<x"
     1.8 +  by (simp add: order_le_less linorder_less_linear)
     1.9 +
    1.10  lemma linorder_le_cases [case_names le ge]:
    1.11      "((x::'a::linorder) \<le> y ==> P) ==> (y \<le> x ==> P) ==> P"
    1.12    by (insert linorder_linear, blast)