| changeset 6299 | 1a88db6e7c7e |
| parent 6295 | 351b3c2b0d83 |
| child 6646 | 3ea726909fff |
--- a/src/HOL/UNITY/Comp.ML Wed Mar 03 10:36:24 1999 +0100 +++ b/src/HOL/UNITY/Comp.ML Wed Mar 03 10:50:42 1999 +0100 @@ -181,7 +181,7 @@ qed "guaranteesI"; Goalw [guarantees_def, component_def] - "[| F : X guarantees Y; F Join G : X; compatible{F,G} |] \ + "[| F : X guarantees Y; F Join G : X |] \ \ ==> F Join G : Y"; by (Blast_tac 1); qed "guaranteesD";