src/Pure/Tools/ROOT.ML
changeset 20657 da6e410c5387
parent 20600 6d75e02ed285
child 20708 29c1754b250f
--- a/src/Pure/Tools/ROOT.ML	Thu Sep 21 15:40:31 2006 +0200
+++ b/src/Pure/Tools/ROOT.ML	Thu Sep 21 15:40:49 2006 +0200
@@ -31,3 +31,6 @@
 use "nbe_eval.ML";
 use "nbe_codegen.ML";
 use "nbe.ML";
+
+(*XML syntax for terms and types*)
+use "xml_syntax.ML";