new (unused) lemma

--- a/src/HOL/UNITY/Extend.ML	Wed Aug 16 10:22:41 2000 +0200
+++ b/src/HOL/UNITY/Extend.ML	Wed Aug 16 10:23:25 2000 +0200
@@ -233,6 +233,11 @@
 by Auto_tac;
 qed "project_set_extend_set_Int";
 
+(*Unused, but interesting?*)
+Goal "project_set h ((extend_set h A) Un B) = A Un (project_set h B)";
+by Auto_tac;
+qed "project_set_extend_set_Un";
+
 Goal "project_set h (A Int B) <= (project_set h A) Int (project_set h B)";
 by Auto_tac;
 qed "project_set_Int_subset";