src/Pure/ROOT
author wenzelm
Tue Apr 05 15:58:58 2016 +0200 (2016-04-05)
changeset 62868 61a691db1c4d
parent 62866 d20262cd20e8
child 62880 76e7d9169b54
permissions -rw-r--r--
support for ML project ROOT file, with imitation of ML "use" commands;
wenzelm@51397
     1
chapter Pure
wenzelm@51397
     2
wenzelm@48738
     3
session Pure =
wenzelm@62868
     4
  global_theories
wenzelm@62868
     5
    Pure
wenzelm@62868
     6
  theories
wenzelm@62868
     7
    "ML/ML_Root"
wenzelm@62868
     8
  files
wenzelm@62868
     9
    "ROOT.ML"