# HG changeset patch
# User paulson
# Date 936004823 -7200
# Node ID 1048bc161c050f92eb561854219329ff432060a0
# Parent  1d486a5b6176530f4205d12d77fd0580f0bbc654
a new theorem

diff -r 1d486a5b6176 -r 1048bc161c05 src/HOL/UNITY/Comp.ML
--- a/src/HOL/UNITY/Comp.ML	Mon Aug 30 11:13:27 1999 +0200
+++ b/src/HOL/UNITY/Comp.ML	Mon Aug 30 11:20:23 1999 +0200
@@ -71,6 +71,10 @@
 by (Blast_tac 1);
 qed "Join_component_iff";
 
+Goal "[| F component G; G : A co B |] ==> F : A co B";
+by (auto_tac (claset(), 
+	      simpset() addsimps [constrains_def, component_eq_subset]));
+qed "component_constrains";
 
 (*** existential properties ***)