--- a/src/HOL/Makefile Fri Jun 30 11:34:14 1995 +0200
+++ b/src/HOL/Makefile Fri Jun 30 11:39:20 1995 +0200
@@ -108,7 +108,8 @@
echo 'exit_use"Lambda/ROOT.ML";quit();' | $(LOGIC)
##Miscellaneous examples
-EX_NAMES = LexProd MT Acc PropLog Puzzle Qsort LList Rec Simult Term String
+EX_NAMES = LexProd MT Acc PropLog Puzzle Qsort LList Rec Simult Term String \
+ BT Perm
EX_FILES = ex/ROOT.ML ex/cla.ML ex/meson.ML ex/mesontest.ML ex/rel.ML \
ex/set.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML)
--- a/src/HOL/ex/ROOT.ML Fri Jun 30 11:34:14 1995 +0200
+++ b/src/HOL/ex/ROOT.ML Fri Jun 30 11:39:20 1995 +0200
@@ -15,6 +15,8 @@
time_use "ex/meson.ML";
time_use "ex/mesontest.ML";
time_use_thy "String";
+time_use_thy "BT";
+time_use_thy "Perm";
time_use_thy "InSort";
time_use_thy "Qsort";
time_use_thy "LexProd";