simplified ensures_UNIV
authorpaulson
Wed Nov 25 15:54:41 1998 +0100 (1998-11-25)
changeset 5971c5a7a7685826
parent 5970 44ff61e1fe82
child 5972 2430ccbde87d
simplified ensures_UNIV
src/HOL/UNITY/WFair.ML
     1.1 --- a/src/HOL/UNITY/WFair.ML	Wed Nov 25 15:53:31 1998 +0100
     1.2 +++ b/src/HOL/UNITY/WFair.ML	Wed Nov 25 15:54:41 1998 +0100
     1.3 @@ -53,7 +53,7 @@
     1.4  qed "ensures_weaken_R";
     1.5  
     1.6  Goalw [ensures_def, constrains_def, transient_def]
     1.7 -    "Acts F ~= {} ==> F : ensures A UNIV";
     1.8 +    "F : ensures A UNIV";
     1.9  by Auto_tac;
    1.10  qed "ensures_UNIV";
    1.11