author  wenzelm 
Sat, 05 Mar 2016 13:53:08 +0100  
changeset 62517  091fdc002a52 
parent 62516  5732f1c31566 
child 62519  a564458f94db 
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 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

4 
global_theories Pure 
48514  5 
files 
6 
"Concurrent/bash.ML" 

60962
faa452d8e265
basic setup for native Windows (RAW session without image);
wenzelm
parents:
60923
diff
changeset

7 
"Concurrent/bash_windows.ML" 
48514  8 
"Concurrent/cache.ML" 
60908  9 
"Concurrent/counter.ML" 
52050  10 
"Concurrent/event_timer.ML" 
48514  11 
"Concurrent/future.ML" 
12 
"Concurrent/lazy.ML" 

13 
"Concurrent/mailbox.ML" 

62508
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62505
diff
changeset

14 
"Concurrent/multithreading.ML" 
48514  15 
"Concurrent/par_exn.ML" 
16 
"Concurrent/par_list.ML" 

59172  17 
"Concurrent/random.ML" 
48514  18 
"Concurrent/single_assignment.ML" 
61556  19 
"Concurrent/standard_thread.ML" 
48514  20 
"Concurrent/synchronized.ML" 
21 
"Concurrent/task_queue.ML" 

22 
"Concurrent/time_limit.ML" 

62508
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62505
diff
changeset

23 
"Concurrent/unsynchronized.ML" 
48514  24 
"General/alist.ML" 
25 
"General/antiquote.ML" 

26 
"General/balanced_tree.ML" 

27 
"General/basics.ML" 

28 
"General/binding.ML" 

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

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

31 
"General/completion.ML" 
62508
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62505
diff
changeset

32 
"General/exn.ML" 
48514  33 
"General/file.ML" 
34 
"General/graph.ML" 

49561  35 
"General/graph_display.ML" 
48514  36 
"General/heap.ML" 
59064  37 
"General/input.ML" 
48514  38 
"General/integer.ML" 
39 
"General/linear_set.ML" 

40 
"General/long_name.ML" 

41 
"General/name_space.ML" 

42 
"General/ord_list.ML" 

43 
"General/output.ML" 

44 
"General/path.ML" 

45 
"General/position.ML" 

46 
"General/pretty.ML" 

47 
"General/print_mode.ML" 

48 
"General/properties.ML" 

49 
"General/queue.ML" 

50 
"General/same.ML" 

51 
"General/scan.ML" 

62508
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62505
diff
changeset

52 
"General/secure.ML" 
48514  53 
"General/seq.ML" 
54 
"General/sha1.ML" 

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

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

57 
"General/socket_io.ML" 
48514  58 
"General/source.ML" 
59 
"General/stack.ML" 

60 
"General/symbol.ML" 

61 
"General/symbol_pos.ML" 

62 
"General/table.ML" 

63 
"General/timing.ML" 

64 
"General/url.ML" 

65 
"Isar/args.ML" 

66 
"Isar/attrib.ML" 

67 
"Isar/auto_bind.ML" 

68 
"Isar/bundle.ML" 

69 
"Isar/class.ML" 

70 
"Isar/class_declaration.ML" 

71 
"Isar/code.ML" 

72 
"Isar/context_rules.ML" 

73 
"Isar/element.ML" 

59901  74 
"Isar/experiment.ML" 
48514  75 
"Isar/expression.ML" 
76 
"Isar/generic_target.ML" 

61677  77 
"Isar/interpretation.ML" 
48514  78 
"Isar/isar_cmd.ML" 
79 
"Isar/keyword.ML" 

80 
"Isar/local_defs.ML" 

81 
"Isar/local_theory.ML" 

82 
"Isar/locale.ML" 

83 
"Isar/method.ML" 

84 
"Isar/named_target.ML" 

85 
"Isar/object_logic.ML" 

86 
"Isar/obtain.ML" 

87 
"Isar/outer_syntax.ML" 

88 
"Isar/overloading.ML" 

89 
"Isar/parse.ML" 

90 
"Isar/parse_spec.ML" 

91 
"Isar/proof.ML" 

92 
"Isar/proof_context.ML" 

93 
"Isar/proof_display.ML" 

94 
"Isar/proof_node.ML" 

95 
"Isar/rule_cases.ML" 

96 
"Isar/runtime.ML" 

97 
"Isar/spec_rules.ML" 

98 
"Isar/specification.ML" 

60630  99 
"Isar/subgoal.ML" 
48514  100 
"Isar/token.ML" 
101 
"Isar/toplevel.ML" 

102 
"Isar/typedecl.ML" 

62498  103 
"ML/exn_debugger.ML" 
62355  104 
"ML/exn_properties.ML" 
62508
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62505
diff
changeset

105 
"ML/fixed_int_dummy.ML" 
48514  106 
"ML/install_pp_polyml.ML" 
56072  107 
"ML/ml_antiquotation.ML" 
62355  108 
"ML/ml_compiler.ML" 
62508
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62505
diff
changeset

109 
"ML/ml_compiler0.ML" 
48514  110 
"ML/ml_context.ML" 
62508
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62505
diff
changeset

111 
"ML/ml_debugger.ML" 
48514  112 
"ML/ml_env.ML" 
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58846
diff
changeset

113 
"ML/ml_file.ML" 
62508
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62505
diff
changeset

114 
"ML/ml_heap.ML" 
48514  115 
"ML/ml_lex.ML" 
62508
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62505
diff
changeset

116 
"ML/ml_name_space.ML" 
60908  117 
"ML/ml_options.ML" 
62508
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62505
diff
changeset

118 
"ML/ml_pretty.ML" 
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62505
diff
changeset

119 
"ML/ml_profiling.ML" 
62459  120 
"ML/ml_statistics.ML" 
48514  121 
"ML/ml_syntax.ML" 
62508
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62505
diff
changeset

122 
"ML/ml_system.ML" 
50450
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50255
diff
changeset

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

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

127 
"PIDE/document_id.ML" 
52605  128 
"PIDE/execution.ML" 
48514  129 
"PIDE/markup.ML" 
130 
"PIDE/protocol.ML" 

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

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

132 
"PIDE/query_operation.ML" 
56208  133 
"PIDE/resources.ML" 
56210  134 
"PIDE/session.ML" 
48514  135 
"PIDE/xml.ML" 
136 
"PIDE/yxml.ML" 

137 
"Proof/extraction.ML" 

138 
"Proof/proof_checker.ML" 

139 
"Proof/proof_rewrite_rules.ML" 

140 
"Proof/proof_syntax.ML" 

141 
"Proof/reconstruct.ML" 

142 
"ROOT.ML" 

143 
"Syntax/ast.ML" 

144 
"Syntax/lexicon.ML" 

145 
"Syntax/local_syntax.ML" 

146 
"Syntax/mixfix.ML" 

147 
"Syntax/parser.ML" 

148 
"Syntax/printer.ML" 

149 
"Syntax/simple_syntax.ML" 

150 
"Syntax/syntax.ML" 

151 
"Syntax/syntax_ext.ML" 

152 
"Syntax/syntax_phases.ML" 

153 
"Syntax/syntax_trans.ML" 

154 
"Syntax/term_position.ML" 

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

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

156 
"System/command_line.ML" 
48514  157 
"System/invoke_scala.ML" 
158 
"System/isabelle_process.ML" 

159 
"System/isabelle_system.ML" 

52584  160 
"System/message_channel.ML" 
48514  161 
"System/options.ML" 
162 
"System/system_channel.ML" 

61619  163 
"Thy/document_antiquotations.ML" 
48514  164 
"Thy/html.ML" 
165 
"Thy/latex.ML" 

61441  166 
"Thy/markdown.ML" 
48514  167 
"Thy/present.ML" 
168 
"Thy/term_style.ML" 

169 
"Thy/thy_header.ML" 

170 
"Thy/thy_info.ML" 

171 
"Thy/thy_output.ML" 

172 
"Thy/thy_syntax.ML" 

50686  173 
"Tools/build.ML" 
48514  174 
"Tools/named_thms.ML" 
58660  175 
"Tools/plugin.ML" 
48514  176 
"assumption.ML" 
177 
"axclass.ML" 

178 
"config.ML" 

179 
"conjunction.ML" 

180 
"consts.ML" 

181 
"context.ML" 

182 
"context_position.ML" 

183 
"conv.ML" 

184 
"defs.ML" 

185 
"drule.ML" 

186 
"envir.ML" 

187 
"facts.ML" 

188 
"global_theory.ML" 

189 
"goal.ML" 

190 
"goal_display.ML" 

191 
"item_net.ML" 

192 
"library.ML" 

193 
"logic.ML" 

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

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

196 
"more_unify.ML" 
48514  197 
"morphism.ML" 
198 
"name.ML" 

199 
"net.ML" 

58009  200 
"par_tactical.ML" 
48514  201 
"pattern.ML" 
202 
"primitive_defs.ML" 

203 
"proofterm.ML" 

48879  204 
"pure_syn.ML" 
48514  205 
"pure_thy.ML" 
206 
"raw_simplifier.ML" 

207 
"search.ML" 

208 
"sign.ML" 

209 
"simplifier.ML" 

51551  210 
"skip_proof.ML" 
48514  211 
"sorts.ML" 
212 
"tactic.ML" 

213 
"tactical.ML" 

214 
"term.ML" 

215 
"term_ord.ML" 

216 
"term_sharing.ML" 

217 
"term_subst.ML" 

218 
"term_xml.ML" 

219 
"theory.ML" 

220 
"thm.ML" 

221 
"type.ML" 

222 
"type_infer.ML" 

223 
"type_infer_context.ML" 

224 
"unify.ML" 

225 
"variable.ML" 