new rule

--- a/src/HOL/UNITY/Comp.ML	Tue Oct 13 10:32:59 1998 +0200
+++ b/src/HOL/UNITY/Comp.ML	Tue Oct 13 10:50:41 1998 +0200
@@ -158,6 +158,10 @@
 by (blast_tac (claset() addIs prems) 1);
 qed "guaranteesI";
 
+Goal "[| F : A guarantees B;  F Join G : A |] ==> F Join G : B";
+by (asm_full_simp_tac (simpset() addsimps [guarantees_eq]) 1);
+qed "guaranteesD";
+
 
 (*** well-definedness ***)