changeset 3511 | da4dd8b7ced4 |
parent 2237 | f01ac387e82b |
child 3929 | 3553fcfa2c7e |
--- a/src/CTT/ROOT.ML Wed Jul 09 16:54:17 1997 +0200 +++ b/src/CTT/ROOT.ML Wed Jul 09 17:00:34 1997 +0200 @@ -12,15 +12,12 @@ print_depth 1; -init_thy_reader(); - use_thy "CTT"; use "../Provers/typedsimp.ML"; use "rew.ML"; use_thy "Arith"; use_thy "Bool"; -init_pps (); print_depth 8; val CTT_build_completed = (); (*indicate successful build*)