98 Recdef.thy Reconstruction.thy Record.thy Relation.ML Relation.thy \ |
98 Recdef.thy Reconstruction.thy Record.thy Relation.ML Relation.thy \ |
99 Relation_Power.thy LOrder.thy OrderedGroup.thy OrderedGroup.ML \ |
99 Relation_Power.thy LOrder.thy OrderedGroup.thy OrderedGroup.ML \ |
100 Orderings.ML Orderings.thy Ring_and_Field.thy\ |
100 Orderings.ML Orderings.thy Ring_and_Field.thy\ |
101 Set.ML Set.thy SetInterval.thy \ |
101 Set.ML Set.thy SetInterval.thy \ |
102 Sum_Type.thy Tools/datatype_abs_proofs.ML Tools/datatype_aux.ML \ |
102 Sum_Type.thy Tools/datatype_abs_proofs.ML Tools/datatype_aux.ML \ |
103 Tools/datatype_codegen.ML Tools/datatype_package.ML Tools/datatype_prop.ML \ |
103 Tools/datatype_codegen.ML Tools/datatype_package.ML Tools/datatype_prop.ML \ |
104 Tools/datatype_realizer.ML Tools/datatype_rep_proofs.ML \ |
104 Tools/datatype_realizer.ML Tools/datatype_rep_proofs.ML \ |
105 Tools/inductive_codegen.ML Tools/inductive_package.ML Tools/inductive_realizer.ML \ |
105 Tools/inductive_codegen.ML Tools/inductive_package.ML Tools/inductive_realizer.ML \ |
106 Tools/meson.ML Tools/numeral_syntax.ML \ |
106 Tools/meson.ML Tools/numeral_syntax.ML \ |
107 Tools/primrec_package.ML Tools/prop_logic.ML \ |
107 Tools/primrec_package.ML Tools/prop_logic.ML \ |
108 Tools/recdef_package.ML Tools/recfun_codegen.ML Tools/record_package.ML \ |
108 Tools/recdef_package.ML Tools/recfun_codegen.ML Tools/record_package.ML \ |
109 Tools/reconstruction.ML Tools/refute.ML Tools/refute_isar.ML \ |
109 Tools/reconstruction.ML Tools/refute.ML Tools/refute_isar.ML \ |
110 Tools/rewrite_hol_proof.ML Tools/sat_solver.ML Tools/specification_package.ML \ |
110 Tools/rewrite_hol_proof.ML Tools/sat_solver.ML Tools/specification_package.ML \ |
111 Tools/split_rule.ML Tools/typedef_package.ML \ |
111 Tools/split_rule.ML Tools/typedef_package.ML \ |
112 Transitive_Closure.thy Transitive_Closure.ML Typedef.thy \ |
112 Transitive_Closure.thy Transitive_Closure.ML Typedef.thy \ |
113 Wellfounded_Recursion.thy Wellfounded_Relations.thy arith_data.ML antisym_setup.ML \ |
113 Wellfounded_Recursion.thy Wellfounded_Relations.thy arith_data.ML antisym_setup.ML \ |
114 blastdata.ML cladata.ML \ |
114 blastdata.ML cladata.ML \ |
115 Tools/res_lib.ML Tools/res_clause.ML Tools/res_skolem_function.ML\ |
115 Tools/res_lib.ML Tools/res_clause.ML Tools/res_skolem_function.ML\ |
116 Tools/res_axioms.ML Tools/res_types_sorts.ML \ |
116 Tools/res_axioms.ML Tools/res_types_sorts.ML \ |
117 Tools/ATP/recon_prelim.ML Tools/ATP/recon_gandalf_base.ML Tools/ATP/recon_order_clauses.ML\ |
117 Tools/ATP/recon_prelim.ML Tools/ATP/recon_gandalf_base.ML Tools/ATP/recon_order_clauses.ML\ |
118 Tools/ATP/recon_translate_proof.ML Tools/ATP/recon_parse.ML Tools/ATP/recon_reconstruct_proof.ML \ |
118 Tools/ATP/recon_translate_proof.ML Tools/ATP/recon_parse.ML Tools/ATP/recon_reconstruct_proof.ML \ |
119 Tools/ATP/recon_transfer_proof.ML Tools/ATP/myres_axioms.ML Tools/ATP/res_clasimpset.ML \ |
119 Tools/ATP/recon_transfer_proof.ML Tools/ATP/res_clasimpset.ML \ |
120 Tools/ATP/VampireCommunication.ML Tools/ATP/SpassCommunication.ML Tools/ATP/modUnix.ML \ |
120 Tools/ATP/VampireCommunication.ML Tools/ATP/SpassCommunication.ML Tools/ATP/modUnix.ML \ |
121 Tools/ATP/watcher.sig Tools/ATP/watcher.ML Tools/res_atp.ML\ |
121 Tools/ATP/watcher.sig Tools/ATP/watcher.ML Tools/res_atp.ML\ |
122 document/root.tex hologic.ML simpdata.ML thy_syntax.ML |
122 document/root.tex hologic.ML simpdata.ML thy_syntax.ML |
123 @$(ISATOOL) usedir -b -g true $(HOL_PROOF_OBJECTS) $(OUT)/Pure HOL |
123 @$(ISATOOL) usedir -b -g true $(HOL_PROOF_OBJECTS) $(OUT)/Pure HOL |
124 |
124 |
125 |
125 |
126 ## HOL-Complex-HahnBanach |
126 ## HOL-Complex-HahnBanach |