src/HOL/Induct/ROOT.ML
changeset 14288 d149e3cbdb39
parent 13075 d3e1d554cd6d
child 14505 e2373489d373
--- a/src/HOL/Induct/ROOT.ML	Wed Dec 10 14:29:44 2003 +0100
+++ b/src/HOL/Induct/ROOT.ML	Wed Dec 10 15:59:34 2003 +0100
@@ -9,3 +9,6 @@
 time_use_thy "PropLog";
 time_use_thy "SList";
 time_use_thy "LFilter";
+
+time_use_thy "BinaryTree_Map";
+time_use_thy "BinaryTree_TacticStyle";