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.
Set.thy was too specific
authorpaulson
Sat, 01 Nov 1997 13:00:03 +0100
changeset 4060 600f266eac45
parent 4059 59c1422c9da5
child 4061 5a2cc5752cb6
Set.thy was too specific
src/HOL/Subst/Subst.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Subst/Subst.ML	Sat Nov 01 12:59:06 1997 +0100
+++ b/src/HOL/Subst/Subst.ML	Sat Nov 01 13:00:03 1997 +0100
@@ -153,7 +153,7 @@
 by (Blast_tac 1);
 qed "srange_iff";
 
-goalw Set.thy [empty_def] "(A = {}) = (ALL a.~ a:A)";
+goalw thy [empty_def] "(A = {}) = (ALL a.~ a:A)";
 by (Blast_tac 1);
 qed "empty_iff_all_not";
isabelle