src/HOL/ROOT.ML
changeset 1515 4ed79ebab64d
parent 1496 c443b2adaf52
child 1982 38aafcab6890
--- a/src/HOL/ROOT.ML	Mon Feb 19 13:54:15 1996 +0100
+++ b/src/HOL/ROOT.ML	Mon Feb 19 18:04:41 1996 +0100
@@ -29,7 +29,6 @@
 use     "typedef.ML";
 use_thy "Sum";
 use_thy "Gfp";
-use_thy "RelPow";
 
 use "datatype.ML";
 use "ind_syntax.ML";
@@ -38,6 +37,7 @@
 use "indrule.ML";
 use_thy "Inductive";
 
+use_thy "RelPow";
 use_thy "Finite";
 use_thy "Sexp";
 use_thy "List";