| author | wenzelm |
| Sat, 03 Oct 2015 18:38:25 +0200 | |
| changeset 61320 | 69022bbcd012 |
| parent 61268 | abe08fb15a12 |
| child 61441 | 20ff1d5c74e1 |
| permissions | -rw-r--r-- |
|
51397
03b586ee5930
support for 'chapter' specifications within session ROOT;
wenzelm
parents:
50911
diff
changeset
|
1 |
chapter Pure |
|
03b586ee5930
support for 'chapter' specifications within session ROOT;
wenzelm
parents:
50911
diff
changeset
|
2 |
|
|
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48732
diff
changeset
|
3 |
session RAW = |
| 48916 | 4 |
theories |
| 48347 | 5 |
files |
6 |
"General/exn.ML" |
|
7 |
"ML-Systems/compiler_polyml.ML" |
|
| 59470 | 8 |
"ML-Systems/exn_trace_polyml-5.5.1.ML" |
|
60745
d86b4cd0f1ec
clarified ML compiler parameters: always provide PolyML.Compiler.CPDebug, ignore global default;
wenzelm
parents:
60731
diff
changeset
|
9 |
"ML-Systems/ml_compiler_parameters.ML" |
|
d86b4cd0f1ec
clarified ML compiler parameters: always provide PolyML.Compiler.CPDebug, ignore global default;
wenzelm
parents:
60731
diff
changeset
|
10 |
"ML-Systems/ml_compiler_parameters_polyml-5.5.3.ML" |
|
d86b4cd0f1ec
clarified ML compiler parameters: always provide PolyML.Compiler.CPDebug, ignore global default;
wenzelm
parents:
60731
diff
changeset
|
11 |
"ML-Systems/ml_debugger.ML" |
| 60729 | 12 |
"ML-Systems/ml_debugger_polyml-5.5.3.ML" |
| 48347 | 13 |
"ML-Systems/ml_name_space.ML" |
|
60731
4ac4b314d93c
additional ML parse tree components for Poly/ML 5.5.3, or later;
wenzelm
parents:
60729
diff
changeset
|
14 |
"ML-Systems/ml_parse_tree.ML" |
|
4ac4b314d93c
additional ML parse tree components for Poly/ML 5.5.3, or later;
wenzelm
parents:
60729
diff
changeset
|
15 |
"ML-Systems/ml_parse_tree_polyml-5.5.3.ML" |
|
56435
28b34e8e4a80
approximate ML antiquotation @{here} for Isabelle/Pure bootstrap;
wenzelm
parents:
56303
diff
changeset
|
16 |
"ML-Systems/ml_positions.ML" |
| 48347 | 17 |
"ML-Systems/ml_pretty.ML" |
| 60923 | 18 |
"ML-Systems/ml_stack_dummy.ML" |
19 |
"ML-Systems/ml_stack_polyml-5.5.3.ML" |
|
| 48347 | 20 |
"ML-Systems/ml_system.ML" |
21 |
"ML-Systems/multithreading.ML" |
|
22 |
"ML-Systems/multithreading_polyml.ML" |
|
23 |
"ML-Systems/overloading_smlnj.ML" |
|
|
54723
124432e77ecf
simplified polyml-5.5.2 setup -- implicit upgrade of Thread.numProcessors;
wenzelm
parents:
54717
diff
changeset
|
24 |
"ML-Systems/polyml-5.5.2.ML" |
|
58470
890d8286fd4e
pro-forma support for polyml-5.5.3 (presently SVN 1960);
wenzelm
parents:
58009
diff
changeset
|
25 |
"ML-Systems/polyml-5.5.3.ML" |
|
60731
4ac4b314d93c
additional ML parse tree components for Poly/ML 5.5.3, or later;
wenzelm
parents:
60729
diff
changeset
|
26 |
"ML-Systems/polyml.ML" |
| 48347 | 27 |
"ML-Systems/pp_dummy.ML" |
28 |
"ML-Systems/proper_int.ML" |
|
|
60731
4ac4b314d93c
additional ML parse tree components for Poly/ML 5.5.3, or later;
wenzelm
parents:
60729
diff
changeset
|
29 |
"ML-Systems/share_common_data_polyml-5.3.0.ML" |
| 48347 | 30 |
"ML-Systems/single_assignment.ML" |
31 |
"ML-Systems/single_assignment_polyml.ML" |
|
32 |
"ML-Systems/smlnj.ML" |
|
33 |
"ML-Systems/thread_dummy.ML" |
|
34 |
"ML-Systems/universal.ML" |
|
35 |
"ML-Systems/unsynchronized.ML" |
|
36 |
"ML-Systems/use_context.ML" |
|
| 60993 | 37 |
"ML-Systems/windows_path.ML" |
| 48347 | 38 |
|
|
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48732
diff
changeset
|
39 |
session Pure = |
|
56801
8dd9df88f647
some support for session-qualified theories: allow to refer to resources via qualified name instead of odd file-system path;
wenzelm
parents:
56435
diff
changeset
|
40 |
global_theories Pure |
| 48514 | 41 |
files |
42 |
"General/exn.ML" |
|
43 |
"ML-Systems/compiler_polyml.ML" |
|
| 59470 | 44 |
"ML-Systems/exn_trace_polyml-5.5.1.ML" |
|
60745
d86b4cd0f1ec
clarified ML compiler parameters: always provide PolyML.Compiler.CPDebug, ignore global default;
wenzelm
parents:
60731
diff
changeset
|
45 |
"ML-Systems/ml_compiler_parameters.ML" |
|
d86b4cd0f1ec
clarified ML compiler parameters: always provide PolyML.Compiler.CPDebug, ignore global default;
wenzelm
parents:
60731
diff
changeset
|
46 |
"ML-Systems/ml_compiler_parameters_polyml-5.5.3.ML" |
|
d86b4cd0f1ec
clarified ML compiler parameters: always provide PolyML.Compiler.CPDebug, ignore global default;
wenzelm
parents:
60731
diff
changeset
|
47 |
"ML-Systems/ml_debugger.ML" |
|
60731
4ac4b314d93c
additional ML parse tree components for Poly/ML 5.5.3, or later;
wenzelm
parents:
60729
diff
changeset
|
48 |
"ML-Systems/ml_debugger_polyml-5.5.3.ML" |
| 48514 | 49 |
"ML-Systems/ml_name_space.ML" |
|
60731
4ac4b314d93c
additional ML parse tree components for Poly/ML 5.5.3, or later;
wenzelm
parents:
60729
diff
changeset
|
50 |
"ML-Systems/ml_parse_tree.ML" |
|
4ac4b314d93c
additional ML parse tree components for Poly/ML 5.5.3, or later;
wenzelm
parents:
60729
diff
changeset
|
51 |
"ML-Systems/ml_parse_tree_polyml-5.5.3.ML" |
|
56435
28b34e8e4a80
approximate ML antiquotation @{here} for Isabelle/Pure bootstrap;
wenzelm
parents:
56303
diff
changeset
|
52 |
"ML-Systems/ml_positions.ML" |
| 48514 | 53 |
"ML-Systems/ml_pretty.ML" |
| 60923 | 54 |
"ML-Systems/ml_stack_dummy.ML" |
55 |
"ML-Systems/ml_stack_polyml-5.5.3.ML" |
|
| 48514 | 56 |
"ML-Systems/ml_system.ML" |
57 |
"ML-Systems/multithreading.ML" |
|
58 |
"ML-Systems/multithreading_polyml.ML" |
|
59 |
"ML-Systems/overloading_smlnj.ML" |
|
|
54723
124432e77ecf
simplified polyml-5.5.2 setup -- implicit upgrade of Thread.numProcessors;
wenzelm
parents:
54717
diff
changeset
|
60 |
"ML-Systems/polyml-5.5.2.ML" |
|
58470
890d8286fd4e
pro-forma support for polyml-5.5.3 (presently SVN 1960);
wenzelm
parents:
58009
diff
changeset
|
61 |
"ML-Systems/polyml-5.5.3.ML" |
|
60731
4ac4b314d93c
additional ML parse tree components for Poly/ML 5.5.3, or later;
wenzelm
parents:
60729
diff
changeset
|
62 |
"ML-Systems/polyml.ML" |
| 48514 | 63 |
"ML-Systems/pp_dummy.ML" |
64 |
"ML-Systems/proper_int.ML" |
|
|
60731
4ac4b314d93c
additional ML parse tree components for Poly/ML 5.5.3, or later;
wenzelm
parents:
60729
diff
changeset
|
65 |
"ML-Systems/share_common_data_polyml-5.3.0.ML" |
| 48514 | 66 |
"ML-Systems/single_assignment.ML" |
67 |
"ML-Systems/single_assignment_polyml.ML" |
|
68 |
"ML-Systems/smlnj.ML" |
|
69 |
"ML-Systems/thread_dummy.ML" |
|
70 |
"ML-Systems/universal.ML" |
|
71 |
"ML-Systems/unsynchronized.ML" |
|
72 |
"ML-Systems/use_context.ML" |
|
| 60993 | 73 |
"ML-Systems/windows_path.ML" |
| 48347 | 74 |
|
| 48514 | 75 |
"Concurrent/bash.ML" |
76 |
"Concurrent/bash_sequential.ML" |
|
|
60962
faa452d8e265
basic setup for native Windows (RAW session without image);
wenzelm
parents:
60923
diff
changeset
|
77 |
"Concurrent/bash_windows.ML" |
| 48514 | 78 |
"Concurrent/cache.ML" |
| 60908 | 79 |
"Concurrent/counter.ML" |
| 52050 | 80 |
"Concurrent/event_timer.ML" |
| 48514 | 81 |
"Concurrent/future.ML" |
82 |
"Concurrent/lazy.ML" |
|
83 |
"Concurrent/lazy_sequential.ML" |
|
84 |
"Concurrent/mailbox.ML" |
|
85 |
"Concurrent/par_exn.ML" |
|
86 |
"Concurrent/par_list.ML" |
|
87 |
"Concurrent/par_list_sequential.ML" |
|
| 59172 | 88 |
"Concurrent/random.ML" |
| 48514 | 89 |
"Concurrent/simple_thread.ML" |
90 |
"Concurrent/single_assignment.ML" |
|
91 |
"Concurrent/single_assignment_sequential.ML" |
|
92 |
"Concurrent/synchronized.ML" |
|
93 |
"Concurrent/synchronized_sequential.ML" |
|
94 |
"Concurrent/task_queue.ML" |
|
95 |
"Concurrent/time_limit.ML" |
|
96 |
"General/alist.ML" |
|
97 |
"General/antiquote.ML" |
|
98 |
"General/balanced_tree.ML" |
|
99 |
"General/basics.ML" |
|
100 |
"General/binding.ML" |
|
101 |
"General/buffer.ML" |
|
|
56053
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
55672
diff
changeset
|
102 |
"General/change_table.ML" |
|
55672
5e25cc741ab9
support for completion within the formal context;
wenzelm
parents:
55516
diff
changeset
|
103 |
"General/completion.ML" |
| 48514 | 104 |
"General/file.ML" |
105 |
"General/graph.ML" |
|
| 49561 | 106 |
"General/graph_display.ML" |
| 48514 | 107 |
"General/heap.ML" |
| 59064 | 108 |
"General/input.ML" |
| 48514 | 109 |
"General/integer.ML" |
110 |
"General/linear_set.ML" |
|
111 |
"General/long_name.ML" |
|
112 |
"General/name_space.ML" |
|
113 |
"General/ord_list.ML" |
|
114 |
"General/output.ML" |
|
115 |
"General/path.ML" |
|
116 |
"General/position.ML" |
|
117 |
"General/pretty.ML" |
|
118 |
"General/print_mode.ML" |
|
119 |
"General/properties.ML" |
|
120 |
"General/queue.ML" |
|
121 |
"General/same.ML" |
|
122 |
"General/scan.ML" |
|
123 |
"General/secure.ML" |
|
124 |
"General/seq.ML" |
|
125 |
"General/sha1.ML" |
|
126 |
"General/sha1_polyml.ML" |
|
|
53212
387b9f7cb0ac
added SHA1 library integrity test, which is invoked at compile time and Isabelle_Process run-time;
wenzelm
parents:
52926
diff
changeset
|
127 |
"General/sha1_samples.ML" |
|
50800
c0fb2839d1a9
recovered buffered sockets from 11f622794ad6 -- requires Poly/ML 5.5.x;
wenzelm
parents:
50686
diff
changeset
|
128 |
"General/socket_io.ML" |
| 48514 | 129 |
"General/source.ML" |
130 |
"General/stack.ML" |
|
131 |
"General/symbol.ML" |
|
132 |
"General/symbol_pos.ML" |
|
133 |
"General/table.ML" |
|
134 |
"General/timing.ML" |
|
135 |
"General/url.ML" |
|
136 |
"Isar/args.ML" |
|
137 |
"Isar/attrib.ML" |
|
138 |
"Isar/auto_bind.ML" |
|
139 |
"Isar/bundle.ML" |
|
140 |
"Isar/class.ML" |
|
141 |
"Isar/class_declaration.ML" |
|
142 |
"Isar/code.ML" |
|
143 |
"Isar/context_rules.ML" |
|
144 |
"Isar/element.ML" |
|
| 59901 | 145 |
"Isar/experiment.ML" |
| 48514 | 146 |
"Isar/expression.ML" |
147 |
"Isar/generic_target.ML" |
|
148 |
"Isar/isar_cmd.ML" |
|
149 |
"Isar/keyword.ML" |
|
150 |
"Isar/local_defs.ML" |
|
151 |
"Isar/local_theory.ML" |
|
152 |
"Isar/locale.ML" |
|
153 |
"Isar/method.ML" |
|
154 |
"Isar/named_target.ML" |
|
155 |
"Isar/object_logic.ML" |
|
156 |
"Isar/obtain.ML" |
|
157 |
"Isar/outer_syntax.ML" |
|
158 |
"Isar/overloading.ML" |
|
159 |
"Isar/parse.ML" |
|
160 |
"Isar/parse_spec.ML" |
|
161 |
"Isar/proof.ML" |
|
162 |
"Isar/proof_context.ML" |
|
163 |
"Isar/proof_display.ML" |
|
164 |
"Isar/proof_node.ML" |
|
165 |
"Isar/rule_cases.ML" |
|
166 |
"Isar/runtime.ML" |
|
167 |
"Isar/spec_rules.ML" |
|
168 |
"Isar/specification.ML" |
|
| 60630 | 169 |
"Isar/subgoal.ML" |
| 48514 | 170 |
"Isar/token.ML" |
171 |
"Isar/toplevel.ML" |
|
172 |
"Isar/typedecl.ML" |
|
|
56303
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56210
diff
changeset
|
173 |
"ML/exn_output.ML" |
|
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56210
diff
changeset
|
174 |
"ML/exn_output_polyml.ML" |
| 52010 | 175 |
"ML/exn_properties_dummy.ML" |
176 |
"ML/exn_properties_polyml.ML" |
|
| 48514 | 177 |
"ML/install_pp_polyml.ML" |
| 56072 | 178 |
"ML/ml_antiquotation.ML" |
| 48514 | 179 |
"ML/ml_compiler.ML" |
180 |
"ML/ml_compiler_polyml.ML" |
|
181 |
"ML/ml_context.ML" |
|
182 |
"ML/ml_env.ML" |
|
|
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58846
diff
changeset
|
183 |
"ML/ml_file.ML" |
| 48514 | 184 |
"ML/ml_lex.ML" |
| 60908 | 185 |
"ML/ml_options.ML" |
| 48514 | 186 |
"ML/ml_parse.ML" |
| 50255 | 187 |
"ML/ml_statistics_dummy.ML" |
188 |
"ML/ml_statistics_polyml-5.5.0.ML" |
|
| 48514 | 189 |
"ML/ml_syntax.ML" |
|
50450
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50255
diff
changeset
|
190 |
"PIDE/active.ML" |
| 48514 | 191 |
"PIDE/command.ML" |
|
57905
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
56801
diff
changeset
|
192 |
"PIDE/command_span.ML" |
| 48514 | 193 |
"PIDE/document.ML" |
|
52530
99dd8b4ef3fe
explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents:
52211
diff
changeset
|
194 |
"PIDE/document_id.ML" |
| 52605 | 195 |
"PIDE/execution.ML" |
| 48514 | 196 |
"PIDE/markup.ML" |
197 |
"PIDE/protocol.ML" |
|
|
59714
ae322325adbb
tuned protocol -- resolve command positions in ML;
wenzelm
parents:
59470
diff
changeset
|
198 |
"PIDE/protocol_message.ML" |
|
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
52836
diff
changeset
|
199 |
"PIDE/query_operation.ML" |
| 56208 | 200 |
"PIDE/resources.ML" |
| 56210 | 201 |
"PIDE/session.ML" |
| 48514 | 202 |
"PIDE/xml.ML" |
203 |
"PIDE/yxml.ML" |
|
204 |
"Proof/extraction.ML" |
|
205 |
"Proof/proof_checker.ML" |
|
206 |
"Proof/proof_rewrite_rules.ML" |
|
207 |
"Proof/proof_syntax.ML" |
|
208 |
"Proof/reconstruct.ML" |
|
209 |
"ROOT.ML" |
|
210 |
"Syntax/ast.ML" |
|
211 |
"Syntax/lexicon.ML" |
|
212 |
"Syntax/local_syntax.ML" |
|
213 |
"Syntax/mixfix.ML" |
|
214 |
"Syntax/parser.ML" |
|
215 |
"Syntax/printer.ML" |
|
216 |
"Syntax/simple_syntax.ML" |
|
217 |
"Syntax/syntax.ML" |
|
218 |
"Syntax/syntax_ext.ML" |
|
219 |
"Syntax/syntax_phases.ML" |
|
220 |
"Syntax/syntax_trans.ML" |
|
221 |
"Syntax/term_position.ML" |
|
|
52211
66bc827e37f8
explicit support for type annotations within printed syntax trees;
wenzelm
parents:
52050
diff
changeset
|
222 |
"Syntax/type_annotation.ML" |
|
48681
181b91e1d1c1
prefer general Command_Line.tool wrapper (cf. Scala version);
wenzelm
parents:
48646
diff
changeset
|
223 |
"System/command_line.ML" |
| 48514 | 224 |
"System/invoke_scala.ML" |
225 |
"System/isabelle_process.ML" |
|
226 |
"System/isabelle_system.ML" |
|
| 52584 | 227 |
"System/message_channel.ML" |
| 48514 | 228 |
"System/options.ML" |
229 |
"System/system_channel.ML" |
|
230 |
"Thy/html.ML" |
|
231 |
"Thy/latex.ML" |
|
232 |
"Thy/present.ML" |
|
233 |
"Thy/term_style.ML" |
|
234 |
"Thy/thy_header.ML" |
|
235 |
"Thy/thy_info.ML" |
|
236 |
"Thy/thy_output.ML" |
|
237 |
"Thy/thy_syntax.ML" |
|
| 50686 | 238 |
"Tools/build.ML" |
| 48514 | 239 |
"Tools/named_thms.ML" |
| 58660 | 240 |
"Tools/plugin.ML" |
| 48514 | 241 |
"assumption.ML" |
242 |
"axclass.ML" |
|
243 |
"config.ML" |
|
244 |
"conjunction.ML" |
|
245 |
"consts.ML" |
|
246 |
"context.ML" |
|
247 |
"context_position.ML" |
|
248 |
"conv.ML" |
|
249 |
"defs.ML" |
|
250 |
"drule.ML" |
|
251 |
"envir.ML" |
|
252 |
"facts.ML" |
|
253 |
"global_theory.ML" |
|
254 |
"goal.ML" |
|
255 |
"goal_display.ML" |
|
256 |
"item_net.ML" |
|
257 |
"library.ML" |
|
258 |
"logic.ML" |
|
|
59026
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
58928
diff
changeset
|
259 |
"more_pattern.ML" |
| 48514 | 260 |
"more_thm.ML" |
|
59026
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
58928
diff
changeset
|
261 |
"more_unify.ML" |
| 48514 | 262 |
"morphism.ML" |
263 |
"name.ML" |
|
264 |
"net.ML" |
|
| 58009 | 265 |
"par_tactical.ML" |
| 48514 | 266 |
"pattern.ML" |
267 |
"primitive_defs.ML" |
|
268 |
"proofterm.ML" |
|
| 48879 | 269 |
"pure_syn.ML" |
| 48514 | 270 |
"pure_thy.ML" |
271 |
"raw_simplifier.ML" |
|
272 |
"search.ML" |
|
273 |
"sign.ML" |
|
274 |
"simplifier.ML" |
|
| 51551 | 275 |
"skip_proof.ML" |
| 48514 | 276 |
"sorts.ML" |
277 |
"tactic.ML" |
|
278 |
"tactical.ML" |
|
279 |
"term.ML" |
|
280 |
"term_ord.ML" |
|
281 |
"term_sharing.ML" |
|
282 |
"term_subst.ML" |
|
283 |
"term_xml.ML" |
|
284 |
"theory.ML" |
|
285 |
"thm.ML" |
|
286 |
"type.ML" |
|
287 |
"type_infer.ML" |
|
288 |
"type_infer_context.ML" |
|
289 |
"unify.ML" |
|
290 |
"variable.ML" |