author  wenzelm 
Tue, 01 Mar 2016 19:42:59 +0100  
changeset 62490  39d01eaf5292 
parent 62468  d97e13e5ea5b 
child 62493  dd154240a53c 
permissions  rwrr 
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 
62077  6 
"RAW/ROOT_polyml5.6.ML" 
7 
"RAW/ROOT_polyml.ML" 

61925  8 
"RAW/compiler_polyml.ML" 
9 
"RAW/exn.ML" 

62459  10 
"RAW/exn_trace.ML" 
62460  11 
"RAW/exn_trace_raw.ML" 
62387
ad3eb2889f9a
support for polymlgit ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents:
62359
diff
changeset

12 
"RAW/fixed_int_dummy.ML" 
61925  13 
"RAW/ml_compiler_parameters.ML" 
14 
"RAW/ml_compiler_parameters_polyml5.6.ML" 

15 
"RAW/ml_debugger.ML" 

16 
"RAW/ml_debugger_polyml5.6.ML" 

62467  17 
"RAW/ml_heap.ML" 
18 
"RAW/ml_heap_polyml5.3.0.ML" 

61925  19 
"RAW/ml_name_space_polyml5.6.ML" 
20 
"RAW/ml_name_space_polyml.ML" 

21 
"RAW/ml_parse_tree.ML" 

22 
"RAW/ml_parse_tree_polyml5.6.ML" 

23 
"RAW/ml_positions.ML" 

24 
"RAW/ml_pretty.ML" 

25 
"RAW/ml_profiling_polyml5.6.ML" 

26 
"RAW/ml_profiling_polyml.ML" 

27 
"RAW/ml_stack_dummy.ML" 

28 
"RAW/ml_stack_polyml5.6.ML" 

29 
"RAW/ml_system.ML" 

30 
"RAW/multithreading.ML" 

31 
"RAW/single_assignment_polyml.ML" 

32 
"RAW/unsynchronized.ML" 

48347  33 

48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48732
diff
changeset

34 
session Pure = 
56801
8dd9df88f647
some support for sessionqualified theories: allow to refer to resources via qualified name instead of odd filesystem path;
wenzelm
parents:
56435
diff
changeset

35 
global_theories Pure 
48514  36 
files 
62077  37 
"RAW/ROOT_polyml5.6.ML" 
38 
"RAW/ROOT_polyml.ML" 

61925  39 
"RAW/compiler_polyml.ML" 
40 
"RAW/exn.ML" 

62459  41 
"RAW/exn_trace.ML" 
62460  42 
"RAW/exn_trace_raw.ML" 
62387
ad3eb2889f9a
support for polymlgit ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents:
62359
diff
changeset

43 
"RAW/fixed_int_dummy.ML" 
61925  44 
"RAW/ml_compiler_parameters.ML" 
45 
"RAW/ml_compiler_parameters_polyml5.6.ML" 

46 
"RAW/ml_debugger.ML" 

47 
"RAW/ml_debugger_polyml5.6.ML" 

62467  48 
"RAW/ml_heap.ML" 
49 
"RAW/ml_heap_polyml5.3.0.ML" 

61925  50 
"RAW/ml_name_space_polyml5.6.ML" 
51 
"RAW/ml_name_space_polyml.ML" 

52 
"RAW/ml_parse_tree.ML" 

53 
"RAW/ml_parse_tree_polyml5.6.ML" 

54 
"RAW/ml_positions.ML" 

55 
"RAW/ml_pretty.ML" 

56 
"RAW/ml_profiling_polyml5.6.ML" 

57 
"RAW/ml_profiling_polyml.ML" 

58 
"RAW/ml_stack_dummy.ML" 

59 
"RAW/ml_stack_polyml5.6.ML" 

60 
"RAW/ml_system.ML" 

61 
"RAW/multithreading.ML" 

62 
"RAW/single_assignment_polyml.ML" 

63 
"RAW/unsynchronized.ML" 

48347  64 

48514  65 
"Concurrent/bash.ML" 
60962
faa452d8e265
basic setup for native Windows (RAW session without image);
wenzelm
parents:
60923
diff
changeset

66 
"Concurrent/bash_windows.ML" 
48514  67 
"Concurrent/cache.ML" 
60908  68 
"Concurrent/counter.ML" 
52050  69 
"Concurrent/event_timer.ML" 
48514  70 
"Concurrent/future.ML" 
71 
"Concurrent/lazy.ML" 

72 
"Concurrent/mailbox.ML" 

73 
"Concurrent/par_exn.ML" 

74 
"Concurrent/par_list.ML" 

59172  75 
"Concurrent/random.ML" 
48514  76 
"Concurrent/single_assignment.ML" 
61556  77 
"Concurrent/standard_thread.ML" 
48514  78 
"Concurrent/synchronized.ML" 
79 
"Concurrent/task_queue.ML" 

80 
"Concurrent/time_limit.ML" 

81 
"General/alist.ML" 

82 
"General/antiquote.ML" 

83 
"General/balanced_tree.ML" 

84 
"General/basics.ML" 

85 
"General/binding.ML" 

86 
"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

87 
"General/change_table.ML" 
55672
5e25cc741ab9
support for completion within the formal context;
wenzelm
parents:
55516
diff
changeset

88 
"General/completion.ML" 
48514  89 
"General/file.ML" 
90 
"General/graph.ML" 

49561  91 
"General/graph_display.ML" 
48514  92 
"General/heap.ML" 
59064  93 
"General/input.ML" 
48514  94 
"General/integer.ML" 
95 
"General/linear_set.ML" 

96 
"General/long_name.ML" 

97 
"General/name_space.ML" 

98 
"General/ord_list.ML" 

99 
"General/output.ML" 

100 
"General/path.ML" 

101 
"General/position.ML" 

102 
"General/pretty.ML" 

103 
"General/print_mode.ML" 

104 
"General/properties.ML" 

105 
"General/queue.ML" 

106 
"General/same.ML" 

107 
"General/scan.ML" 

108 
"General/secure.ML" 

109 
"General/seq.ML" 

110 
"General/sha1.ML" 

111 
"General/sha1_polyml.ML" 

53212
387b9f7cb0ac
added SHA1 library integrity test, which is invoked at compile time and Isabelle_Process runtime;
wenzelm
parents:
52926
diff
changeset

112 
"General/sha1_samples.ML" 
50800
c0fb2839d1a9
recovered buffered sockets from 11f622794ad6  requires Poly/ML 5.5.x;
wenzelm
parents:
50686
diff
changeset

113 
"General/socket_io.ML" 
48514  114 
"General/source.ML" 
115 
"General/stack.ML" 

116 
"General/symbol.ML" 

117 
"General/symbol_pos.ML" 

118 
"General/table.ML" 

119 
"General/timing.ML" 

120 
"General/url.ML" 

121 
"Isar/args.ML" 

122 
"Isar/attrib.ML" 

123 
"Isar/auto_bind.ML" 

124 
"Isar/bundle.ML" 

125 
"Isar/class.ML" 

126 
"Isar/class_declaration.ML" 

127 
"Isar/code.ML" 

128 
"Isar/context_rules.ML" 

129 
"Isar/element.ML" 

59901  130 
"Isar/experiment.ML" 
48514  131 
"Isar/expression.ML" 
132 
"Isar/generic_target.ML" 

61677  133 
"Isar/interpretation.ML" 
48514  134 
"Isar/isar_cmd.ML" 
135 
"Isar/keyword.ML" 

136 
"Isar/local_defs.ML" 

137 
"Isar/local_theory.ML" 

138 
"Isar/locale.ML" 

139 
"Isar/method.ML" 

140 
"Isar/named_target.ML" 

141 
"Isar/object_logic.ML" 

142 
"Isar/obtain.ML" 

143 
"Isar/outer_syntax.ML" 

144 
"Isar/overloading.ML" 

145 
"Isar/parse.ML" 

146 
"Isar/parse_spec.ML" 

147 
"Isar/proof.ML" 

148 
"Isar/proof_context.ML" 

149 
"Isar/proof_display.ML" 

150 
"Isar/proof_node.ML" 

151 
"Isar/rule_cases.ML" 

152 
"Isar/runtime.ML" 

153 
"Isar/spec_rules.ML" 

154 
"Isar/specification.ML" 

60630  155 
"Isar/subgoal.ML" 
48514  156 
"Isar/token.ML" 
157 
"Isar/toplevel.ML" 

158 
"Isar/typedecl.ML" 

62355  159 
"ML/exn_output.ML" 
160 
"ML/exn_properties.ML" 

48514  161 
"ML/install_pp_polyml.ML" 
56072  162 
"ML/ml_antiquotation.ML" 
62355  163 
"ML/ml_compiler.ML" 
48514  164 
"ML/ml_context.ML" 
165 
"ML/ml_env.ML" 

58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58846
diff
changeset

166 
"ML/ml_file.ML" 
48514  167 
"ML/ml_lex.ML" 
60908  168 
"ML/ml_options.ML" 
48514  169 
"ML/ml_parse.ML" 
62459  170 
"ML/ml_statistics.ML" 
50255  171 
"ML/ml_statistics_dummy.ML" 
48514  172 
"ML/ml_syntax.ML" 
50450
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50255
diff
changeset

173 
"PIDE/active.ML" 
48514  174 
"PIDE/command.ML" 
57905
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
56801
diff
changeset

175 
"PIDE/command_span.ML" 
48514  176 
"PIDE/document.ML" 
52530
99dd8b4ef3fe
explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents:
52211
diff
changeset

177 
"PIDE/document_id.ML" 
52605  178 
"PIDE/execution.ML" 
48514  179 
"PIDE/markup.ML" 
180 
"PIDE/protocol.ML" 

59714
ae322325adbb
tuned protocol  resolve command positions in ML;
wenzelm
parents:
59470
diff
changeset

181 
"PIDE/protocol_message.ML" 
52865
02a7e7180ee5
slightly more general support for oneshot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
52836
diff
changeset

182 
"PIDE/query_operation.ML" 
56208  183 
"PIDE/resources.ML" 
56210  184 
"PIDE/session.ML" 
48514  185 
"PIDE/xml.ML" 
186 
"PIDE/yxml.ML" 

187 
"Proof/extraction.ML" 

188 
"Proof/proof_checker.ML" 

189 
"Proof/proof_rewrite_rules.ML" 

190 
"Proof/proof_syntax.ML" 

191 
"Proof/reconstruct.ML" 

192 
"ROOT.ML" 

193 
"Syntax/ast.ML" 

194 
"Syntax/lexicon.ML" 

195 
"Syntax/local_syntax.ML" 

196 
"Syntax/mixfix.ML" 

197 
"Syntax/parser.ML" 

198 
"Syntax/printer.ML" 

199 
"Syntax/simple_syntax.ML" 

200 
"Syntax/syntax.ML" 

201 
"Syntax/syntax_ext.ML" 

202 
"Syntax/syntax_phases.ML" 

203 
"Syntax/syntax_trans.ML" 

204 
"Syntax/term_position.ML" 

52211
66bc827e37f8
explicit support for type annotations within printed syntax trees;
wenzelm
parents:
52050
diff
changeset

205 
"Syntax/type_annotation.ML" 
48681
181b91e1d1c1
prefer general Command_Line.tool wrapper (cf. Scala version);
wenzelm
parents:
48646
diff
changeset

206 
"System/command_line.ML" 
48514  207 
"System/invoke_scala.ML" 
208 
"System/isabelle_process.ML" 

209 
"System/isabelle_system.ML" 

52584  210 
"System/message_channel.ML" 
48514  211 
"System/options.ML" 
212 
"System/system_channel.ML" 

61619  213 
"Thy/document_antiquotations.ML" 
48514  214 
"Thy/html.ML" 
215 
"Thy/latex.ML" 

61441  216 
"Thy/markdown.ML" 
48514  217 
"Thy/present.ML" 
218 
"Thy/term_style.ML" 

219 
"Thy/thy_header.ML" 

220 
"Thy/thy_info.ML" 

221 
"Thy/thy_output.ML" 

222 
"Thy/thy_syntax.ML" 

50686  223 
"Tools/build.ML" 
48514  224 
"Tools/named_thms.ML" 
58660  225 
"Tools/plugin.ML" 
48514  226 
"assumption.ML" 
227 
"axclass.ML" 

228 
"config.ML" 

229 
"conjunction.ML" 

230 
"consts.ML" 

231 
"context.ML" 

232 
"context_position.ML" 

233 
"conv.ML" 

234 
"defs.ML" 

235 
"drule.ML" 

236 
"envir.ML" 

237 
"facts.ML" 

238 
"global_theory.ML" 

239 
"goal.ML" 

240 
"goal_display.ML" 

241 
"item_net.ML" 

242 
"library.ML" 

243 
"logic.ML" 

59026
30b8a5825a9c
removed some addons from modules that are relevant for the inference kernel;
wenzelm
parents:
58928
diff
changeset

244 
"more_pattern.ML" 
48514  245 
"more_thm.ML" 
59026
30b8a5825a9c
removed some addons from modules that are relevant for the inference kernel;
wenzelm
parents:
58928
diff
changeset

246 
"more_unify.ML" 
48514  247 
"morphism.ML" 
248 
"name.ML" 

249 
"net.ML" 

58009  250 
"par_tactical.ML" 
48514  251 
"pattern.ML" 
252 
"primitive_defs.ML" 

253 
"proofterm.ML" 

48879  254 
"pure_syn.ML" 
48514  255 
"pure_thy.ML" 
256 
"raw_simplifier.ML" 

257 
"search.ML" 

258 
"sign.ML" 

259 
"simplifier.ML" 

51551  260 
"skip_proof.ML" 
48514  261 
"sorts.ML" 
262 
"tactic.ML" 

263 
"tactical.ML" 

264 
"term.ML" 

265 
"term_ord.ML" 

266 
"term_sharing.ML" 

267 
"term_subst.ML" 

268 
"term_xml.ML" 

269 
"theory.ML" 

270 
"thm.ML" 

271 
"type.ML" 

272 
"type_infer.ML" 

273 
"type_infer_context.ML" 

274 
"unify.ML" 

275 
"variable.ML" 