17 LOG = $(OUT)/log |
17 LOG = $(OUT)/log |
18 |
18 |
19 |
19 |
20 ## Pure |
20 ## Pure |
21 |
21 |
22 BOOTSTRAP_FILES = ML-Systems/bash.ML ML-Systems/compiler_polyml-5.0.ML \ |
22 BOOTSTRAP_FILES = \ |
23 ML-Systems/compiler_polyml-5.2.ML ML-Systems/compiler_polyml-5.3.ML \ |
23 ML-Systems/bash.ML \ |
24 ML-Systems/ml_name_space.ML ML-Systems/ml_pretty.ML \ |
24 ML-Systems/compiler_polyml-5.0.ML \ |
25 ML-Systems/multithreading.ML ML-Systems/multithreading_polyml.ML \ |
25 ML-Systems/compiler_polyml-5.2.ML \ |
26 ML-Systems/overloading_smlnj.ML ML-Systems/polyml-5.0.ML \ |
26 ML-Systems/compiler_polyml-5.3.ML \ |
27 ML-Systems/polyml-5.1.ML ML-Systems/polyml-5.2.ML \ |
27 ML-Systems/ml_name_space.ML \ |
28 ML-Systems/polyml-5.2.1.ML ML-Systems/polyml.ML \ |
28 ML-Systems/ml_pretty.ML \ |
29 ML-Systems/polyml_common.ML ML-Systems/pp_polyml.ML \ |
29 ML-Systems/multithreading.ML \ |
30 ML-Systems/proper_int.ML ML-Systems/single_assignment.ML \ |
30 ML-Systems/multithreading_polyml.ML \ |
31 ML-Systems/single_assignment_polyml.ML ML-Systems/smlnj.ML \ |
31 ML-Systems/overloading_smlnj.ML \ |
32 ML-Systems/thread_dummy.ML ML-Systems/timing.ML \ |
32 ML-Systems/polyml-5.0.ML \ |
33 ML-Systems/time_limit.ML ML-Systems/universal.ML \ |
33 ML-Systems/polyml-5.1.ML \ |
34 ML-Systems/unsynchronized.ML |
34 ML-Systems/polyml-5.2.1.ML \ |
|
35 ML-Systems/polyml-5.2.ML \ |
|
36 ML-Systems/polyml.ML \ |
|
37 ML-Systems/polyml_common.ML \ |
|
38 ML-Systems/pp_polyml.ML \ |
|
39 ML-Systems/proper_int.ML \ |
|
40 ML-Systems/single_assignment.ML \ |
|
41 ML-Systems/single_assignment_polyml.ML \ |
|
42 ML-Systems/smlnj.ML \ |
|
43 ML-Systems/thread_dummy.ML \ |
|
44 ML-Systems/time_limit.ML \ |
|
45 ML-Systems/timing.ML \ |
|
46 ML-Systems/universal.ML \ |
|
47 ML-Systems/unsynchronized.ML \ |
|
48 ML-Systems/use_context.ML |
35 |
49 |
36 RAW: $(OUT)/RAW |
50 RAW: $(OUT)/RAW |
37 |
51 |
38 $(OUT)/RAW: $(BOOTSTRAP_FILES) |
52 $(OUT)/RAW: $(BOOTSTRAP_FILES) |
39 @./mk -r |
53 @./mk -r |
40 |
54 |
41 |
55 |
42 Pure: $(OUT)/Pure |
56 Pure: $(OUT)/Pure |
43 |
57 |
44 $(OUT)/Pure: $(BOOTSTRAP_FILES) Concurrent/cache.ML \ |
58 $(OUT)/Pure: $(BOOTSTRAP_FILES) \ |
45 Concurrent/future.ML Concurrent/lazy.ML \ |
59 Concurrent/cache.ML \ |
46 Concurrent/lazy_sequential.ML Concurrent/mailbox.ML \ |
60 Concurrent/future.ML \ |
47 Concurrent/par_list.ML Concurrent/par_list_sequential.ML \ |
61 Concurrent/lazy.ML \ |
48 Concurrent/simple_thread.ML Concurrent/single_assignment.ML \ |
62 Concurrent/lazy_sequential.ML \ |
49 Concurrent/single_assignment_sequential.ML \ |
63 Concurrent/mailbox.ML \ |
50 Concurrent/synchronized.ML Concurrent/synchronized_sequential.ML \ |
64 Concurrent/par_list.ML \ |
51 Concurrent/task_queue.ML General/alist.ML General/antiquote.ML \ |
65 Concurrent/par_list_sequential.ML \ |
52 General/balanced_tree.ML General/basics.ML General/binding.ML \ |
66 Concurrent/simple_thread.ML \ |
53 General/buffer.ML General/exn.ML General/file.ML General/graph.ML \ |
67 Concurrent/single_assignment.ML \ |
54 General/heap.ML General/integer.ML General/long_name.ML \ |
68 Concurrent/single_assignment_sequential.ML \ |
55 General/markup.ML General/name_space.ML General/ord_list.ML \ |
69 Concurrent/synchronized.ML \ |
56 General/output.ML General/path.ML General/position.ML \ |
70 Concurrent/synchronized_sequential.ML \ |
57 General/pretty.ML General/print_mode.ML General/properties.ML \ |
71 Concurrent/task_queue.ML \ |
58 General/queue.ML General/same.ML General/scan.ML General/sha1.ML \ |
72 General/alist.ML \ |
59 General/sha1_polyml.ML General/secure.ML General/seq.ML \ |
73 General/antiquote.ML \ |
60 General/source.ML General/stack.ML General/symbol.ML \ |
74 General/balanced_tree.ML \ |
61 General/symbol_pos.ML General/table.ML General/url.ML General/xml.ML \ |
75 General/basics.ML \ |
62 General/xml_data.ML General/yxml.ML Isar/args.ML Isar/attrib.ML \ |
76 General/binding.ML \ |
63 Isar/auto_bind.ML Isar/calculation.ML Isar/class.ML \ |
77 General/buffer.ML \ |
64 Isar/class_target.ML Isar/code.ML Isar/constdefs.ML \ |
78 General/exn.ML \ |
65 Isar/context_rules.ML Isar/element.ML Isar/expression.ML \ |
79 General/file.ML \ |
66 Isar/generic_target.ML Isar/isar_cmd.ML Isar/isar_document.ML \ |
80 General/graph.ML \ |
67 Isar/isar_syn.ML Isar/keyword.ML Isar/local_defs.ML \ |
81 General/heap.ML \ |
68 Isar/local_syntax.ML Isar/local_theory.ML Isar/locale.ML \ |
82 General/integer.ML \ |
69 Isar/method.ML Isar/object_logic.ML Isar/obtain.ML \ |
83 General/long_name.ML \ |
70 Isar/outer_syntax.ML Isar/overloading.ML Isar/parse.ML \ |
84 General/markup.ML \ |
71 Isar/parse_spec.ML Isar/parse_value.ML Isar/proof.ML \ |
85 General/name_space.ML \ |
72 Isar/proof_context.ML Isar/proof_display.ML Isar/proof_node.ML \ |
86 General/ord_list.ML \ |
73 Isar/rule_cases.ML Isar/rule_insts.ML Isar/runtime.ML \ |
87 General/output.ML \ |
74 Isar/skip_proof.ML Isar/spec_rules.ML Isar/specification.ML \ |
88 General/path.ML \ |
75 Isar/theory_target.ML Isar/token.ML Isar/toplevel.ML \ |
89 General/position.ML \ |
76 Isar/typedecl.ML ML/ml_antiquote.ML ML/ml_compiler.ML \ |
90 General/pretty.ML \ |
77 ML/ml_compiler_polyml-5.3.ML ML/ml_context.ML ML/ml_env.ML \ |
91 General/print_mode.ML \ |
78 ML/ml_lex.ML ML/ml_parse.ML ML/ml_syntax.ML ML/ml_thms.ML \ |
92 General/properties.ML \ |
79 ML-Systems/install_pp_polyml.ML ML-Systems/install_pp_polyml-5.3.ML \ |
93 General/queue.ML \ |
80 ML-Systems/use_context.ML Proof/extraction.ML PIDE/document.ML \ |
94 General/same.ML \ |
81 Proof/proof_rewrite_rules.ML Proof/proof_syntax.ML \ |
95 General/scan.ML \ |
82 Proof/proofchecker.ML Proof/reconstruct.ML ProofGeneral/pgip.ML \ |
96 General/secure.ML \ |
83 ProofGeneral/pgip_input.ML ProofGeneral/pgip_isabelle.ML \ |
97 General/seq.ML \ |
84 ProofGeneral/pgip_markup.ML ProofGeneral/pgip_output.ML \ |
98 General/sha1.ML \ |
85 ProofGeneral/pgip_parser.ML ProofGeneral/pgip_tests.ML \ |
99 General/sha1_polyml.ML \ |
86 ProofGeneral/pgip_types.ML ProofGeneral/preferences.ML \ |
100 General/source.ML \ |
87 ProofGeneral/proof_general_emacs.ML General/yxml.ML Isar/args.ML \ |
101 General/stack.ML \ |
88 Isar/attrib.ML Isar/auto_bind.ML Isar/calculation.ML Isar/class.ML \ |
102 General/symbol.ML \ |
89 Isar/class_target.ML Isar/code.ML Isar/constdefs.ML \ |
103 General/symbol_pos.ML \ |
90 Isar/context_rules.ML Isar/element.ML Isar/expression.ML \ |
104 General/table.ML \ |
91 Isar/isar_cmd.ML Isar/isar_document.ML Isar/isar_syn.ML \ |
105 General/url.ML \ |
92 Isar/keyword.ML Isar/local_defs.ML Isar/local_syntax.ML \ |
106 General/xml.ML \ |
93 Isar/local_theory.ML Isar/locale.ML Isar/method.ML \ |
107 General/xml_data.ML \ |
94 Isar/object_logic.ML Isar/obtain.ML Isar/outer_syntax.ML \ |
108 General/yxml.ML \ |
95 Isar/overloading.ML Isar/parse.ML Isar/parse_spec.ML \ |
109 Isar/args.ML \ |
96 Isar/parse_value.ML Isar/proof.ML Isar/proof_context.ML \ |
110 Isar/attrib.ML \ |
97 Isar/proof_display.ML Isar/proof_node.ML Isar/rule_cases.ML \ |
111 Isar/auto_bind.ML \ |
98 Isar/rule_insts.ML Isar/runtime.ML Isar/skip_proof.ML \ |
112 Isar/calculation.ML \ |
99 Isar/spec_rules.ML Isar/specification.ML Isar/theory_target.ML \ |
113 Isar/class.ML \ |
100 Isar/token.ML Isar/toplevel.ML Isar/typedecl.ML ML/ml_antiquote.ML \ |
114 Isar/class_target.ML \ |
101 ML/ml_compiler.ML ML/ml_compiler_polyml-5.3.ML ML/ml_context.ML \ |
115 Isar/code.ML \ |
102 ML/ml_env.ML ML/ml_lex.ML ML/ml_parse.ML ML/ml_syntax.ML \ |
116 Isar/constdefs.ML \ |
103 ML/ml_thms.ML ML-Systems/install_pp_polyml.ML \ |
117 Isar/context_rules.ML \ |
104 ML-Systems/install_pp_polyml-5.3.ML ML-Systems/use_context.ML \ |
118 Isar/element.ML \ |
105 Proof/extraction.ML PIDE/document.ML Proof/proof_rewrite_rules.ML \ |
119 Isar/expression.ML \ |
106 Proof/proof_syntax.ML Proof/proofchecker.ML Proof/reconstruct.ML \ |
120 Isar/generic_target.ML \ |
107 ProofGeneral/pgip.ML ProofGeneral/pgip_input.ML \ |
121 Isar/isar_cmd.ML \ |
108 ProofGeneral/pgip_isabelle.ML ProofGeneral/pgip_markup.ML \ |
122 Isar/isar_document.ML \ |
109 ProofGeneral/pgip_output.ML ProofGeneral/pgip_parser.ML \ |
123 Isar/isar_syn.ML \ |
110 ProofGeneral/pgip_tests.ML ProofGeneral/pgip_types.ML \ |
124 Isar/keyword.ML \ |
111 ProofGeneral/preferences.ML ProofGeneral/proof_general_emacs.ML \ |
125 Isar/local_defs.ML \ |
112 ProofGeneral/proof_general_pgip.ML Pure.thy ROOT.ML Syntax/ast.ML \ |
126 Isar/local_syntax.ML \ |
113 Syntax/lexicon.ML Syntax/mixfix.ML Syntax/parser.ML \ |
127 Isar/local_theory.ML \ |
114 Syntax/printer.ML Syntax/simple_syntax.ML Syntax/syn_ext.ML \ |
128 Isar/locale.ML \ |
115 Syntax/syn_trans.ML Syntax/syntax.ML Syntax/type_ext.ML \ |
129 Isar/method.ML \ |
116 System/isabelle_process.ML System/isar.ML System/session.ML \ |
130 Isar/object_logic.ML \ |
117 Thy/html.ML Thy/latex.ML Thy/present.ML Thy/term_style.ML \ |
131 Isar/obtain.ML \ |
118 Thy/thm_deps.ML Thy/thy_header.ML Thy/thy_info.ML Thy/thy_load.ML \ |
132 Isar/outer_syntax.ML \ |
119 Thy/thy_output.ML Thy/thy_syntax.ML Tools/find_consts.ML \ |
133 Isar/overloading.ML \ |
120 Tools/find_theorems.ML Tools/named_thms.ML Tools/xml_syntax.ML \ |
134 Isar/parse.ML \ |
121 assumption.ML axclass.ML codegen.ML config.ML conjunction.ML \ |
135 Isar/parse_spec.ML \ |
122 consts.ML context.ML context_position.ML conv.ML defs.ML display.ML \ |
136 Isar/parse_value.ML \ |
123 drule.ML envir.ML facts.ML goal.ML goal_display.ML interpretation.ML \ |
137 Isar/proof.ML \ |
124 item_net.ML library.ML logic.ML meta_simplifier.ML more_thm.ML \ |
138 Isar/proof_context.ML \ |
125 morphism.ML name.ML net.ML old_goals.ML old_term.ML pattern.ML \ |
139 Isar/proof_display.ML \ |
126 primitive_defs.ML proofterm.ML pure_setup.ML pure_thy.ML search.ML \ |
140 Isar/proof_node.ML \ |
127 sign.ML simplifier.ML sorts.ML subgoal.ML tactic.ML tactical.ML \ |
141 Isar/rule_cases.ML \ |
128 term.ML term_ord.ML term_subst.ML theory.ML thm.ML type.ML \ |
142 Isar/rule_insts.ML \ |
129 type_infer.ML unify.ML variable.ML |
143 Isar/runtime.ML \ |
|
144 Isar/skip_proof.ML \ |
|
145 Isar/spec_rules.ML \ |
|
146 Isar/specification.ML \ |
|
147 Isar/theory_target.ML \ |
|
148 Isar/token.ML \ |
|
149 Isar/toplevel.ML \ |
|
150 Isar/typedecl.ML \ |
|
151 ML/install_pp_polyml-5.3.ML \ |
|
152 ML/install_pp_polyml.ML \ |
|
153 ML/ml_antiquote.ML \ |
|
154 ML/ml_compiler.ML \ |
|
155 ML/ml_compiler_polyml-5.3.ML \ |
|
156 ML/ml_context.ML \ |
|
157 ML/ml_env.ML \ |
|
158 ML/ml_lex.ML \ |
|
159 ML/ml_parse.ML \ |
|
160 ML/ml_syntax.ML \ |
|
161 ML/ml_thms.ML \ |
|
162 PIDE/document.ML \ |
|
163 Proof/extraction.ML \ |
|
164 Proof/proof_rewrite_rules.ML \ |
|
165 Proof/proof_syntax.ML \ |
|
166 Proof/proofchecker.ML \ |
|
167 Proof/reconstruct.ML \ |
|
168 ProofGeneral/pgip.ML \ |
|
169 ProofGeneral/pgip_input.ML \ |
|
170 ProofGeneral/pgip_isabelle.ML \ |
|
171 ProofGeneral/pgip_markup.ML \ |
|
172 ProofGeneral/pgip_output.ML \ |
|
173 ProofGeneral/pgip_parser.ML \ |
|
174 ProofGeneral/pgip_tests.ML \ |
|
175 ProofGeneral/pgip_types.ML \ |
|
176 ProofGeneral/pgml.ML \ |
|
177 ProofGeneral/preferences.ML \ |
|
178 ProofGeneral/proof_general_emacs.ML \ |
|
179 ProofGeneral/proof_general_pgip.ML \ |
|
180 Pure.thy \ |
|
181 ROOT.ML \ |
|
182 Syntax/ast.ML \ |
|
183 Syntax/lexicon.ML \ |
|
184 Syntax/mixfix.ML \ |
|
185 Syntax/parser.ML \ |
|
186 Syntax/printer.ML \ |
|
187 Syntax/simple_syntax.ML \ |
|
188 Syntax/syn_ext.ML \ |
|
189 Syntax/syn_trans.ML \ |
|
190 Syntax/syntax.ML \ |
|
191 Syntax/type_ext.ML \ |
|
192 System/isabelle_process.ML \ |
|
193 System/isar.ML \ |
|
194 System/session.ML \ |
|
195 Thy/html.ML \ |
|
196 Thy/latex.ML \ |
|
197 Thy/present.ML \ |
|
198 Thy/term_style.ML \ |
|
199 Thy/thm_deps.ML \ |
|
200 Thy/thy_header.ML \ |
|
201 Thy/thy_info.ML \ |
|
202 Thy/thy_load.ML \ |
|
203 Thy/thy_output.ML \ |
|
204 Thy/thy_syntax.ML \ |
|
205 Tools/find_consts.ML \ |
|
206 Tools/find_theorems.ML \ |
|
207 Tools/named_thms.ML \ |
|
208 Tools/xml_syntax.ML \ |
|
209 assumption.ML \ |
|
210 axclass.ML \ |
|
211 codegen.ML \ |
|
212 config.ML \ |
|
213 conjunction.ML \ |
|
214 consts.ML \ |
|
215 context.ML \ |
|
216 context_position.ML \ |
|
217 conv.ML \ |
|
218 defs.ML \ |
|
219 display.ML \ |
|
220 drule.ML \ |
|
221 envir.ML \ |
|
222 facts.ML \ |
|
223 goal.ML \ |
|
224 goal_display.ML \ |
|
225 interpretation.ML \ |
|
226 item_net.ML \ |
|
227 library.ML \ |
|
228 logic.ML \ |
|
229 meta_simplifier.ML \ |
|
230 more_thm.ML \ |
|
231 morphism.ML \ |
|
232 name.ML \ |
|
233 net.ML \ |
|
234 old_goals.ML \ |
|
235 old_term.ML \ |
|
236 pattern.ML \ |
|
237 primitive_defs.ML \ |
|
238 proofterm.ML \ |
|
239 pure_setup.ML \ |
|
240 pure_thy.ML \ |
|
241 search.ML \ |
|
242 sign.ML \ |
|
243 simplifier.ML \ |
|
244 sorts.ML \ |
|
245 subgoal.ML \ |
|
246 tactic.ML \ |
|
247 tactical.ML \ |
|
248 term.ML \ |
|
249 term_ord.ML \ |
|
250 term_subst.ML \ |
|
251 theory.ML \ |
|
252 thm.ML \ |
|
253 type.ML \ |
|
254 type_infer.ML \ |
|
255 unify.ML \ |
|
256 variable.ML |
130 @./mk |
257 @./mk |
131 |
258 |
132 |
259 |
133 ## Proof General keywords |
260 ## Proof General keywords |
134 |
261 |