doc-src/TutorialI/Misc/ROOT.ML
changeset 8745 13b32661dde4
child 9493 494f8cd34df7
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/doc-src/TutorialI/Misc/ROOT.ML	Wed Apr 19 11:56:31 2000 +0200
     1.3 @@ -0,0 +1,18 @@
     1.4 +use_thy "Tree";
     1.5 +use_thy "cases";
     1.6 +use_thy "fakenat";
     1.7 +use_thy "natsum";
     1.8 +use_thy "arith1";
     1.9 +use_thy "arith2";
    1.10 +use_thy "arith3";
    1.11 +use_thy "arith4";
    1.12 +use_thy "pairs";
    1.13 +use_thy "types";
    1.14 +use_thy "prime_def";
    1.15 +use_thy "def_rewr";
    1.16 +use_thy "let_rewr";
    1.17 +use_thy "cond_rewr";
    1.18 +use_thy "case_splits";
    1.19 +use_thy "trace_simp";
    1.20 +use_thy "Itrev";
    1.21 +use_thy "asm_simp";