src/HOL/Library/Disjoint_Sets.thy
changeset 61824 dcbe9f756ae0
parent 60727 53697011b03a
child 62390 842917225d56
     1.1 --- a/src/HOL/Library/Disjoint_Sets.thy	Mon Dec 07 10:49:08 2015 +0100
     1.2 +++ b/src/HOL/Library/Disjoint_Sets.thy	Thu Dec 10 13:38:40 2015 +0000
     1.3 @@ -79,7 +79,7 @@
     1.4    "(\<And>n. A n \<subseteq> A (Suc n)) \<Longrightarrow> disjoint_family (\<lambda>i. A (Suc i) - A i)"
     1.5    using lift_Suc_mono_le[of A]
     1.6    by (auto simp add: disjoint_family_on_def)
     1.7 -     (metis insert_absorb insert_subset le_SucE le_antisym not_leE less_imp_le)
     1.8 +     (metis insert_absorb insert_subset le_SucE le_antisym not_le_imp_less less_imp_le)
     1.9  
    1.10  lemma disjoint_family_on_disjoint_image:
    1.11    "disjoint_family_on A I \<Longrightarrow> disjoint (A ` I)"