Mercurial Mercurial > repos > Old_HOL / 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.
shortened use_thy section taking advantage of dependencies
authornipkow
Tue, 04 Jan 1994 18:33:20 +0100
changeset 28 3e32fa0e779a
parent 27 d08128985789
child 29 9769afcc1c4e
shortened use_thy section taking advantage of dependencies
ROOT.ML file | annotate | diff | comparison | revisions 
--- a/ROOT.ML	Thu Dec 30 10:19:44 1993 +0100
+++ b/ROOT.ML	Tue Jan 04 18:33:20 1994 +0100
@@ -79,15 +79,6 @@
 use_thy "Prod";
 use_thy "Sum";
 use     "mono.ML";
-use_thy "Lfp";
-use_thy "Gfp";
-use_thy "Trancl";
-use_thy "WF";
-use_thy "Nat";
-use_thy "Arith";
-use_thy "Univ";
-use_thy "Sexp";
-use_thy "List";
 use_thy "LList";
 
 use "../Pure/install_pp.ML";
Old_HOL