# HG changeset patch # User paulson # Date 961155704 -7200 # Node ID 090d450af656d73cd8a4004b8efce1fcb9fc30bb # Parent b36787a56a1f795ce4a128a1444ba58c33a9edaa fixed for removal of subset_empty diff -r b36787a56a1f -r 090d450af656 src/HOL/UNITY/WFair.ML --- a/src/HOL/UNITY/WFair.ML Fri Jun 16 13:39:21 2000 +0200 +++ b/src/HOL/UNITY/WFair.ML Fri Jun 16 13:41:44 2000 +0200 @@ -41,7 +41,7 @@ qed "transientE"; Goalw [transient_def] "transient UNIV = {}"; -by Auto_tac; +by (Blast_tac 1); qed "transient_UNIV"; Goalw [transient_def] "transient {} = UNIV";