--- a/doc-src/Tutorial/Datatype/ROOT.ML Mon Nov 29 11:12:19 2004 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,25 +0,0 @@
-use_thy "ABexp";
-use"abgoalind.ML";
-use"autotac.ML";
-result();
-
-use_thy "Term";
-use"tidproof.ML";
-result();
-use"appmap.ML";
-by(induct_tac "ts" 1);
-by(Auto_tac);
-qed"subst_App_map";
-Addsimps [subst_App_map];
-result();
-
-use_thy"Trie";
-use"lookupempty.ML";
-qed "lookup_empty";
-Addsimps [lookup_empty];
-use"trieAdds.ML";
-use"triemain.ML";
-use"trieinduct.ML";
-use"trieexhaust.ML";
-by(Auto_tac);
-result();