doc-src/Tutorial/Datatype/ROOT.ML

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Datatype/ROOT.ML	Thu Nov 12 16:45:40 1998 +0100
@@ -0,0 +1,25 @@
+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();