# HG changeset patch
# User paulson
# Date 966414205 -7200
# Node ID 795baaf96201d83822661931fa4255f6a15522f7
# Parent  a50dcf0475ad9b3ffc7f51104aeb80ad682dd49a
new (unused) lemma

diff -r a50dcf0475ad -r 795baaf96201 src/HOL/UNITY/Extend.ML
--- 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";