src/HOL/UNITY/WFair.ML
changeset 5971 c5a7a7685826
parent 5669 f5d9caafc3bd
child 6012 1894bfc4aee9
--- a/src/HOL/UNITY/WFair.ML	Wed Nov 25 15:53:31 1998 +0100
+++ b/src/HOL/UNITY/WFair.ML	Wed Nov 25 15:54:41 1998 +0100
@@ -53,7 +53,7 @@
 qed "ensures_weaken_R";
 
 Goalw [ensures_def, constrains_def, transient_def]
-    "Acts F ~= {} ==> F : ensures A UNIV";
+    "F : ensures A UNIV";
 by Auto_tac;
 qed "ensures_UNIV";