# HG changeset patch
# User lcp
# Date 804505160 -7200
# Node ID e57a93d41de0ddecfdaaf028f0978d11d9ebeb8e
# Parent  b3f2ddef1438bc2ddc708ad3ea5e2ec55360d5ba
added mention of new theories BT and Perm

diff -r b3f2ddef1438 -r e57a93d41de0 src/HOL/Makefile
--- 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)
diff -r b3f2ddef1438 -r e57a93d41de0 src/HOL/ex/ROOT.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";