changeset 119 | 93dc86ccee28 |
parent 101 | 5f99df1e26c4 |
child 128 | 89669c58e506 |
--- a/ROOT.ML Fri Aug 19 11:19:14 1994 +0200 +++ b/ROOT.ML Fri Aug 19 11:25:16 1994 +0200 @@ -77,13 +77,10 @@ use "simpdata.ML"; use_thy "Ord"; -use_thy "Set"; -use "fun.ML"; -use "subset.ML"; -use "equalities.ML"; +use_thy "subset"; +use_thy "equalities"; use_thy "Prod"; use_thy "Sum"; -use "mono.ML"; use_thy "LList"; use "../Pure/install_pp.ML";