changeset 8944 | 96964d43a472 |
parent 8933 | de96f2982d2c |
child 9000 | c20d58286a51 |
--- a/src/HOL/ex/ROOT.ML Tue May 23 18:29:17 2000 +0200 +++ b/src/HOL/ex/ROOT.ML Wed May 24 12:21:26 2000 +0200 @@ -17,7 +17,7 @@ with_path "../Induct" use_thy "Factorization"; time_use_thy "Primrec"; -time_use "NatSum"; +time_use_thy "NatSum"; time_use "cla.ML"; time_use "meson.ML"; time_use "mesontest.ML";