--- a/src/HOL/UNITY/Comp.ML Mon Oct 19 11:24:55 1998 +0200
+++ b/src/HOL/UNITY/Comp.ML Mon Oct 19 11:25:37 1998 +0200
@@ -100,6 +100,12 @@
(*** guarantees ***)
+(*This equation is more intuitive than the official definition*)
+Goalw [guarantees_def, component_def]
+ "(F : A guarantees B) = (ALL G. F Join G : A --> F Join G : B)";
+by (Blast_tac 1);
+qed "guarantees_eq";
+
Goalw [guarantees_def] "X <= Y ==> X guarantees Y = UNIV";
by (Blast_tac 1);
qed "subset_imp_guarantees";
@@ -148,11 +154,6 @@
by (Blast_tac 1);
qed "ex_guarantees";
-Goalw [guarantees_def, component_def]
- "(F : A guarantees B) = (ALL G. F Join G : A --> F Join G : B)";
-by (Blast_tac 1);
-qed "guarantees_eq";
-
val prems = Goalw [guarantees_def, component_def]
"(!!G. F Join G : A ==> F Join G : B) ==> F : A guarantees B";
by (blast_tac (claset() addIs prems) 1);