added General/balanced_tree.ML;
authorwenzelm
Tue, 19 Jun 2007 23:15:43 +0200
changeset 23420 6f60a90e52e5
parent 23419 8c30dd4b3b22
child 23421 c9007fc4a646
added General/balanced_tree.ML;
src/Pure/General/ROOT.ML
src/Pure/IsaMakefile
--- a/src/Pure/General/ROOT.ML	Tue Jun 19 23:15:38 2007 +0200
+++ b/src/Pure/General/ROOT.ML	Tue Jun 19 23:15:43 2007 +0200
@@ -8,6 +8,7 @@
 use "ord_list.ML";
 use "alist.ML";
 use "table.ML";
+use "balanced_tree.ML";
 use "output.ML";
 use "graph.ML";
 use "heap.ML";
--- a/src/Pure/IsaMakefile	Tue Jun 19 23:15:38 2007 +0200
+++ b/src/Pure/IsaMakefile	Tue Jun 19 23:15:43 2007 +0200
@@ -24,9 +24,9 @@
 Pure: $(OUT)/Pure$(ML_SUFFIX)
 
 $(OUT)/Pure$(ML_SUFFIX): CPure.thy General/ROOT.ML General/alist.ML		\
-  General/basics.ML General/buffer.ML General/file.ML General/graph.ML		\
-  General/heap.ML General/history.ML General/ml_syntax.ML General/name_space.ML	\
-  General/ord_list.ML General/output.ML General/path.ML				\
+  General/basics.ML General/balanced_tree.ML General/buffer.ML General/file.ML	\
+  General/graph.ML General/heap.ML General/history.ML General/ml_syntax.ML	\
+  General/name_space.ML General/ord_list.ML General/output.ML General/path.ML	\
   General/position.ML General/pretty.ML General/scan.ML		                \
   General/secure.ML General/seq.ML General/source.ML General/stack.ML		\
   General/susp.ML General/symbol.ML General/table.ML General/url.ML		\