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";