src/HOL/Wellfounded.thy
changeset 29125 d41182a8135c
parent 28845 cdfc8ef54a99
child 29580 117b88da143c
     1.1 --- a/src/HOL/Wellfounded.thy	Tue Dec 16 00:19:47 2008 +0100
     1.2 +++ b/src/HOL/Wellfounded.thy	Tue Dec 16 08:46:07 2008 +0100
     1.3 @@ -842,6 +842,11 @@
     1.4    qed
     1.5  qed
     1.6  
     1.7 +lemma max_ext_additive: 
     1.8 + "(A, B) \<in> max_ext R \<Longrightarrow> (C, D) \<in> max_ext R \<Longrightarrow>
     1.9 +  (A \<union> C, B \<union> D) \<in> max_ext R"
    1.10 +by (force elim!: max_ext.cases)
    1.11 +
    1.12  
    1.13  definition
    1.14    min_ext :: "('a \<times> 'a) set \<Rightarrow> ('a set \<times> 'a set) set"