# HG changeset patch
# User paulson
# Date 908268641 -7200
# Node ID a06006a320a19c19746399cfe179d0a11e422ae5
# Parent  dd8f30780fa9564bdb5151b23eefe4c2bd95a57a
new rule

diff -r dd8f30780fa9 -r a06006a320a1 src/HOL/UNITY/Comp.ML
--- 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 ***)