src/Pure/ROOT
changeset 62490 39d01eaf5292
parent 62468 d97e13e5ea5b
child 62493 dd154240a53c
equal deleted inserted replaced
62489:36f11bc393a2 62490:39d01eaf5292
    28     "RAW/ml_stack_polyml-5.6.ML"
    28     "RAW/ml_stack_polyml-5.6.ML"
    29     "RAW/ml_system.ML"
    29     "RAW/ml_system.ML"
    30     "RAW/multithreading.ML"
    30     "RAW/multithreading.ML"
    31     "RAW/single_assignment_polyml.ML"
    31     "RAW/single_assignment_polyml.ML"
    32     "RAW/unsynchronized.ML"
    32     "RAW/unsynchronized.ML"
    33     "RAW/use_context.ML"
       
    34 
    33 
    35 session Pure =
    34 session Pure =
    36   global_theories Pure
    35   global_theories Pure
    37   files
    36   files
    38     "RAW/ROOT_polyml-5.6.ML"
    37     "RAW/ROOT_polyml-5.6.ML"
    60     "RAW/ml_stack_polyml-5.6.ML"
    59     "RAW/ml_stack_polyml-5.6.ML"
    61     "RAW/ml_system.ML"
    60     "RAW/ml_system.ML"
    62     "RAW/multithreading.ML"
    61     "RAW/multithreading.ML"
    63     "RAW/single_assignment_polyml.ML"
    62     "RAW/single_assignment_polyml.ML"
    64     "RAW/unsynchronized.ML"
    63     "RAW/unsynchronized.ML"
    65     "RAW/use_context.ML"
       
    66 
    64 
    67     "Concurrent/bash.ML"
    65     "Concurrent/bash.ML"
    68     "Concurrent/bash_windows.ML"
    66     "Concurrent/bash_windows.ML"
    69     "Concurrent/cache.ML"
    67     "Concurrent/cache.ML"
    70     "Concurrent/counter.ML"
    68     "Concurrent/counter.ML"