src/HOL/Wellfounded.thy

--- a/src/HOL/Wellfounded.thy	Tue Dec 16 00:19:47 2008 +0100
+++ b/src/HOL/Wellfounded.thy	Tue Dec 16 08:46:07 2008 +0100
@@ -842,6 +842,11 @@
   qed
 qed
 
+lemma max_ext_additive: 
+ "(A, B) \<in> max_ext R \<Longrightarrow> (C, D) \<in> max_ext R \<Longrightarrow>
+  (A \<union> C, B \<union> D) \<in> max_ext R"
+by (force elim!: max_ext.cases)
+
 
 definition
   min_ext :: "('a \<times> 'a) set \<Rightarrow> ('a set \<times> 'a set) set"