src/Pure/ROOT
changeset 62880 76e7d9169b54
parent 62868 61a691db1c4d
child 62883 b04e9fe29223
equal deleted inserted replaced
62879:4764473c9b8d 62880:76e7d9169b54
     2 
     2 
     3 session Pure =
     3 session Pure =
     4   global_theories
     4   global_theories
     5     Pure
     5     Pure
     6   theories
     6   theories
     7     "ML/ML_Root"
     7     ML_Root
     8   files
     8   files
     9     "ROOT.ML"
     9     "ROOT.ML"