# HG changeset patch
# User paulson
# Date 912005681 -3600
# Node ID c5a7a7685826c7dc88c9ca5535f1b28e7104af04
# Parent  44ff61e1fe8205be4247a8bcd33a06e951bd0168
simplified ensures_UNIV

diff -r 44ff61e1fe82 -r c5a7a7685826 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";