Added xml_syntax.ML
authorberghofe
Thu Sep 21 15:40:49 2006 +0200 (2006-09-21)
changeset 20657da6e410c5387
parent 20656 9de0a076b3fc
child 20658 2586df9fb95a
Added xml_syntax.ML
src/Pure/Tools/ROOT.ML
     1.1 --- a/src/Pure/Tools/ROOT.ML	Thu Sep 21 15:40:31 2006 +0200
     1.2 +++ b/src/Pure/Tools/ROOT.ML	Thu Sep 21 15:40:49 2006 +0200
     1.3 @@ -31,3 +31,6 @@
     1.4  use "nbe_eval.ML";
     1.5  use "nbe_codegen.ML";
     1.6  use "nbe.ML";
     1.7 +
     1.8 +(*XML syntax for terms and types*)
     1.9 +use "xml_syntax.ML";