Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fixed for removal of subset_empty
authorpaulson
Fri, 16 Jun 2000 13:41:44 +0200
changeset 9084 090d450af656
parent 9083 b36787a56a1f
child 9085 5ce73f3cadff
fixed for removal of subset_empty
src/HOL/UNITY/WFair.ML file | annotate | diff | comparison | revisions 
--- 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";
isabelle