fixed for removal of subset_empty
authorpaulson
Fri Jun 16 13:41:44 2000 +0200 (2000-06-16)
changeset 9084090d450af656
parent 9083 b36787a56a1f
child 9085 5ce73f3cadff
fixed for removal of subset_empty
src/HOL/UNITY/WFair.ML
     1.1 --- a/src/HOL/UNITY/WFair.ML	Fri Jun 16 13:39:21 2000 +0200
     1.2 +++ b/src/HOL/UNITY/WFair.ML	Fri Jun 16 13:41:44 2000 +0200
     1.3 @@ -41,7 +41,7 @@
     1.4  qed "transientE";
     1.5  
     1.6  Goalw [transient_def] "transient UNIV = {}";
     1.7 -by Auto_tac;
     1.8 +by (Blast_tac 1); 
     1.9  qed "transient_UNIV";
    1.10  
    1.11  Goalw [transient_def] "transient {} = UNIV";