simplified ensures_UNIV
authorpaulson
Wed, 25 Nov 1998 15:54:41 +0100
changeset 5971 c5a7a7685826
parent 5970 44ff61e1fe82
child 5972 2430ccbde87d
simplified ensures_UNIV
src/HOL/UNITY/WFair.ML
--- 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";