changeset 8122 | b43ad07660b9 |
parent 8065 | 658e0d4e4ed9 |
child 8251 | 9be357df93d4 |
--- a/src/HOL/UNITY/Guar.ML Thu Jan 13 17:29:04 2000 +0100 +++ b/src/HOL/UNITY/Guar.ML Thu Jan 13 17:30:23 2000 +0100 @@ -80,7 +80,7 @@ (*This version of guaranteesD matches more easily in the conclusion The major premise can no longer be F<=H since we need to reason about G*) Goalw [guar_def] - "[| F : X guarantees[v] Y; H : X; F Join G = H; G : preserves v |] \ + "[| F : X guarantees[v] Y; F Join G = H; H : X; G : preserves v |] \ \ ==> H : Y"; by (Blast_tac 1); qed "component_guaranteesD";