equal
deleted
inserted
replaced
1 chapter Pure |
1 chapter Pure |
2 |
2 |
3 session RAW = |
3 session RAW = |
4 theories |
4 theories |
5 files |
5 files |
6 "RAW/ROOT_polyml-5.5.2.ML" |
|
7 "RAW/ROOT_polyml-5.6.ML" |
6 "RAW/ROOT_polyml-5.6.ML" |
8 "RAW/ROOT_polyml.ML" |
7 "RAW/ROOT_polyml.ML" |
9 "RAW/compiler_polyml.ML" |
8 "RAW/compiler_polyml.ML" |
10 "RAW/exn.ML" |
9 "RAW/exn.ML" |
11 "RAW/exn_trace_polyml-5.5.1.ML" |
10 "RAW/exn_trace.ML" |
|
11 "RAW/exn_trace_dummy.ML" |
12 "RAW/fixed_int_dummy.ML" |
12 "RAW/fixed_int_dummy.ML" |
13 "RAW/ml_compiler_parameters.ML" |
13 "RAW/ml_compiler_parameters.ML" |
14 "RAW/ml_compiler_parameters_polyml-5.6.ML" |
14 "RAW/ml_compiler_parameters_polyml-5.6.ML" |
15 "RAW/ml_debugger.ML" |
15 "RAW/ml_debugger.ML" |
16 "RAW/ml_debugger_polyml-5.6.ML" |
16 "RAW/ml_debugger_polyml-5.6.ML" |
33 "RAW/windows_path.ML" |
33 "RAW/windows_path.ML" |
34 |
34 |
35 session Pure = |
35 session Pure = |
36 global_theories Pure |
36 global_theories Pure |
37 files |
37 files |
38 "RAW/ROOT_polyml-5.5.2.ML" |
|
39 "RAW/ROOT_polyml-5.6.ML" |
38 "RAW/ROOT_polyml-5.6.ML" |
40 "RAW/ROOT_polyml.ML" |
39 "RAW/ROOT_polyml.ML" |
41 "RAW/compiler_polyml.ML" |
40 "RAW/compiler_polyml.ML" |
42 "RAW/exn.ML" |
41 "RAW/exn.ML" |
43 "RAW/exn_trace_polyml-5.5.1.ML" |
42 "RAW/exn_trace.ML" |
|
43 "RAW/exn_trace_dummy.ML" |
44 "RAW/fixed_int_dummy.ML" |
44 "RAW/fixed_int_dummy.ML" |
45 "RAW/ml_compiler_parameters.ML" |
45 "RAW/ml_compiler_parameters.ML" |
46 "RAW/ml_compiler_parameters_polyml-5.6.ML" |
46 "RAW/ml_compiler_parameters_polyml-5.6.ML" |
47 "RAW/ml_debugger.ML" |
47 "RAW/ml_debugger.ML" |
48 "RAW/ml_debugger_polyml-5.6.ML" |
48 "RAW/ml_debugger_polyml-5.6.ML" |
167 "ML/ml_env.ML" |
167 "ML/ml_env.ML" |
168 "ML/ml_file.ML" |
168 "ML/ml_file.ML" |
169 "ML/ml_lex.ML" |
169 "ML/ml_lex.ML" |
170 "ML/ml_options.ML" |
170 "ML/ml_options.ML" |
171 "ML/ml_parse.ML" |
171 "ML/ml_parse.ML" |
|
172 "ML/ml_statistics.ML" |
172 "ML/ml_statistics_dummy.ML" |
173 "ML/ml_statistics_dummy.ML" |
173 "ML/ml_statistics_polyml-5.5.0.ML" |
|
174 "ML/ml_syntax.ML" |
174 "ML/ml_syntax.ML" |
175 "PIDE/active.ML" |
175 "PIDE/active.ML" |
176 "PIDE/command.ML" |
176 "PIDE/command.ML" |
177 "PIDE/command_span.ML" |
177 "PIDE/command_span.ML" |
178 "PIDE/document.ML" |
178 "PIDE/document.ML" |