Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Induct/Multiset.ML
changeset 6024 cb87f103d114
parent 5983 79e301a6a51b
child 6162 484adda70b65 
--- a/src/HOL/Induct/Multiset.ML	Fri Dec 11 10:38:51 1998 +0100
+++ b/src/HOL/Induct/Multiset.ML	Fri Dec 11 10:41:53 1998 +0100
@@ -431,7 +431,7 @@
 by(blast_tac (claset() addDs [export lemma3]) 1);
 qed "all_accessible";
 
-Close_locale();
+Close_locale "MSOrd";
 
 Goal "wf(r) ==> wf(mult1 r)";
 by(blast_tac (claset() addIs [acc_wfI, export all_accessible]) 1);
isabelle