src/HOL/HOL.thy
changeset 14365 3d4df8c166ae
parent 14361 ad2f5da643b4
child 14398 c5c47703f763
     1.1 --- a/src/HOL/HOL.thy	Tue Jan 27 09:44:14 2004 +0100
     1.2 +++ b/src/HOL/HOL.thy	Tue Jan 27 15:39:51 2004 +0100
     1.3 @@ -804,10 +804,13 @@
     1.4    apply (insert linorder_linear, blast)
     1.5    done
     1.6  
     1.7 +lemma linorder_le_cases [case_names le ge]:
     1.8 +    "((x::'a::linorder) \<le> y ==> P) ==> (y \<le> x ==> P) ==> P"
     1.9 +  by (insert linorder_linear, blast)
    1.10 +
    1.11  lemma linorder_cases [case_names less equal greater]:
    1.12      "((x::'a::linorder) < y ==> P) ==> (x = y ==> P) ==> (y < x ==> P) ==> P"
    1.13 -  apply (insert linorder_less_linear, blast)
    1.14 -  done
    1.15 +  by (insert linorder_less_linear, blast)
    1.16  
    1.17  lemma linorder_not_less: "!!x::'a::linorder. (~ x < y) = (y <= x)"
    1.18    apply (simp add: order_less_le)