src/HOL/Orderings.thy
changeset 64758 3b33d2fc5fc0
parent 64287 d85d88722745
child 65963 ca1e636fa716
     1.1 --- a/src/HOL/Orderings.thy	Mon Jan 02 18:08:04 2017 +0100
     1.2 +++ b/src/HOL/Orderings.thy	Tue Jan 03 16:48:49 2017 +0000
     1.3 @@ -405,6 +405,10 @@
     1.4  lemma not_le_imp_less: "\<not> y \<le> x \<Longrightarrow> x < y"
     1.5  unfolding not_le .
     1.6  
     1.7 +lemma linorder_less_wlog[case_names less refl sym]:
     1.8 +     "\<lbrakk>\<And>a b. a < b \<Longrightarrow> P a b;  \<And>a. P a a;  \<And>a b. P b a \<Longrightarrow> P a b\<rbrakk> \<Longrightarrow> P a b"
     1.9 +  using antisym_conv3 by blast
    1.10 +
    1.11  text \<open>Dual order\<close>
    1.12  
    1.13  lemma dual_linorder: