equal
deleted
inserted
replaced
167 $(SRC)/Provers/Arith/fast_lin_arith.ML \ |
167 $(SRC)/Provers/Arith/fast_lin_arith.ML \ |
168 $(SRC)/Provers/order.ML \ |
168 $(SRC)/Provers/order.ML \ |
169 $(SRC)/Provers/trancl.ML \ |
169 $(SRC)/Provers/trancl.ML \ |
170 $(SRC)/Tools/Metis/metis.ML \ |
170 $(SRC)/Tools/Metis/metis.ML \ |
171 $(SRC)/Tools/rat.ML \ |
171 $(SRC)/Tools/rat.ML \ |
|
172 ATP.thy \ |
172 Complete_Lattice.thy \ |
173 Complete_Lattice.thy \ |
173 Complete_Partial_Order.thy \ |
174 Complete_Partial_Order.thy \ |
174 Datatype.thy \ |
175 Datatype.thy \ |
175 Extraction.thy \ |
176 Extraction.thy \ |
176 Fields.thy \ |
177 Fields.thy \ |
193 Relation.thy \ |
194 Relation.thy \ |
194 Rings.thy \ |
195 Rings.thy \ |
195 SAT.thy \ |
196 SAT.thy \ |
196 Set.thy \ |
197 Set.thy \ |
197 Sum_Type.thy \ |
198 Sum_Type.thy \ |
|
199 Tools/ATP/atp_problem.ML \ |
|
200 Tools/ATP/atp_proof.ML \ |
|
201 Tools/ATP/atp_reconstruct.ML \ |
|
202 Tools/ATP/atp_systems.ML \ |
|
203 Tools/ATP/atp_translate.ML \ |
|
204 Tools/ATP/atp_util.ML \ |
198 Tools/Datatype/datatype.ML \ |
205 Tools/Datatype/datatype.ML \ |
199 Tools/Datatype/datatype_abs_proofs.ML \ |
206 Tools/Datatype/datatype_abs_proofs.ML \ |
200 Tools/Datatype/datatype_aux.ML \ |
207 Tools/Datatype/datatype_aux.ML \ |
201 Tools/Datatype/datatype_case.ML \ |
208 Tools/Datatype/datatype_case.ML \ |
202 Tools/Datatype/datatype_codegen.ML \ |
209 Tools/Datatype/datatype_codegen.ML \ |
254 |
261 |
255 $(OUT)/HOL-Plain: plain.ML $(PLAIN_DEPENDENCIES) |
262 $(OUT)/HOL-Plain: plain.ML $(PLAIN_DEPENDENCIES) |
256 @$(ISABELLE_TOOL) usedir -b -f plain.ML -g true $(OUT)/Pure HOL-Plain |
263 @$(ISABELLE_TOOL) usedir -b -f plain.ML -g true $(OUT)/Pure HOL-Plain |
257 |
264 |
258 MAIN_DEPENDENCIES = $(PLAIN_DEPENDENCIES) \ |
265 MAIN_DEPENDENCIES = $(PLAIN_DEPENDENCIES) \ |
259 ATP.thy \ |
|
260 Big_Operators.thy \ |
266 Big_Operators.thy \ |
261 Code_Evaluation.thy \ |
267 Code_Evaluation.thy \ |
262 Code_Numeral.thy \ |
268 Code_Numeral.thy \ |
263 Divides.thy \ |
269 Divides.thy \ |
264 DSequence.thy \ |
270 DSequence.thy \ |
297 $(SRC)/Provers/Arith/assoc_fold.ML \ |
303 $(SRC)/Provers/Arith/assoc_fold.ML \ |
298 $(SRC)/Provers/Arith/cancel_numeral_factor.ML \ |
304 $(SRC)/Provers/Arith/cancel_numeral_factor.ML \ |
299 $(SRC)/Provers/Arith/cancel_numerals.ML \ |
305 $(SRC)/Provers/Arith/cancel_numerals.ML \ |
300 $(SRC)/Provers/Arith/combine_numerals.ML \ |
306 $(SRC)/Provers/Arith/combine_numerals.ML \ |
301 $(SRC)/Provers/Arith/extract_common_term.ML \ |
307 $(SRC)/Provers/Arith/extract_common_term.ML \ |
302 Tools/ATP/atp_problem.ML \ |
|
303 Tools/ATP/atp_proof.ML \ |
|
304 Tools/ATP/atp_reconstruct.ML \ |
|
305 Tools/ATP/atp_systems.ML \ |
|
306 Tools/ATP/atp_translate.ML \ |
|
307 Tools/ATP/atp_util.ML \ |
|
308 Tools/choice_specification.ML \ |
308 Tools/choice_specification.ML \ |
309 Tools/code_evaluation.ML \ |
309 Tools/code_evaluation.ML \ |
310 Tools/groebner.ML \ |
310 Tools/groebner.ML \ |
311 Tools/int_arith.ML \ |
311 Tools/int_arith.ML \ |
312 Tools/list_code.ML \ |
312 Tools/list_code.ML \ |