79 $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \ |
78 $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \ |
80 $(SRC)/Provers/eqsubst.ML $(SRC)/Provers/hypsubst.ML \ |
79 $(SRC)/Provers/eqsubst.ML $(SRC)/Provers/hypsubst.ML \ |
81 $(SRC)/Provers/induct_method.ML $(SRC)/Provers/order.ML \ |
80 $(SRC)/Provers/induct_method.ML $(SRC)/Provers/order.ML \ |
82 $(SRC)/Provers/project_rule.ML $(SRC)/Provers/quantifier1.ML \ |
81 $(SRC)/Provers/project_rule.ML $(SRC)/Provers/quantifier1.ML \ |
83 $(SRC)/Provers/quasi.ML $(SRC)/Provers/splitter.ML \ |
82 $(SRC)/Provers/quasi.ML $(SRC)/Provers/splitter.ML \ |
84 $(SRC)/Provers/trancl.ML $(SRC)/TFL/casesplit.ML $(SRC)/TFL/dcterm.ML \ |
83 $(SRC)/Provers/trancl.ML $(SRC)/Pure/General/int.ML \ |
85 $(SRC)/TFL/post.ML $(SRC)/TFL/rules.ML $(SRC)/TFL/tfl.ML \ |
84 $(SRC)/Pure/General/rat.ML $(SRC)/TFL/casesplit.ML \ |
86 $(SRC)/TFL/thms.ML $(SRC)/TFL/thry.ML $(SRC)/TFL/usyntax.ML \ |
85 $(SRC)/TFL/dcterm.ML $(SRC)/TFL/post.ML $(SRC)/TFL/rules.ML \ |
87 $(SRC)/TFL/utils.ML ATP_Linkup.thy Accessible_Part.thy \ |
86 $(SRC)/TFL/tfl.ML $(SRC)/TFL/thms.ML $(SRC)/TFL/thry.ML \ |
88 Code_Generator.thy Datatype.thy Divides.thy Equiv_Relations.thy \ |
87 $(SRC)/TFL/usyntax.ML $(SRC)/TFL/utils.ML ATP_Linkup.thy \ |
89 Extraction.thy Finite_Set.thy FixedPoint.thy Fun.thy FunDef.thy \ |
88 Accessible_Part.thy Code_Generator.thy Datatype.thy Divides.thy \ |
90 HOL.thy Hilbert_Choice.thy Inductive.thy Integ/IntArith.thy \ |
89 Equiv_Relations.thy Extraction.thy Finite_Set.thy FixedPoint.thy \ |
91 Integ/IntDef.thy Integ/IntDiv.thy Integ/NatBin.thy \ |
90 Fun.thy FunDef.thy HOL.thy Hilbert_Choice.thy Inductive.thy \ |
92 Integ/NatSimprocs.thy Integ/Numeral.thy Integ/Presburger.thy \ |
91 Integ/IntArith.thy Integ/IntDef.thy Integ/IntDiv.thy Integ/NatBin.thy \ |
93 Integ/cooper_dec.ML Integ/cooper_proof.ML Integ/int_arith1.ML \ |
92 Integ/NatSimprocs.thy Integ/Numeral.thy Integ/int_arith1.ML \ |
94 Integ/int_factor_simprocs.ML Integ/nat_simprocs.ML Integ/presburger.ML \ |
93 Integ/int_factor_simprocs.ML Integ/nat_simprocs.ML Lattices.thy \ |
95 Integ/qelim.ML Integ/reflected_cooper.ML Integ/reflected_presburger.ML \ |
94 List.thy Main.thy Map.thy Nat.ML Nat.thy OrderedGroup.thy \ |
96 Lattices.thy List.thy Main.thy Map.thy Nat.ML Nat.thy \ |
95 Orderings.thy Power.thy PreList.thy Predicate.thy Presburger.thy \ |
97 OrderedGroup.thy Orderings.thy Power.thy Predicate.thy PreList.thy \ |
|
98 Product_Type.thy ROOT.ML Recdef.thy Record.thy Refute.thy Relation.thy \ |
96 Product_Type.thy ROOT.ML Recdef.thy Record.thy Refute.thy Relation.thy \ |
99 Relation_Power.thy Ring_and_Field.thy SAT.thy Set.thy SetInterval.thy \ |
97 Relation_Power.thy Ring_and_Field.thy SAT.thy Set.thy SetInterval.thy \ |
100 Sum_Type.thy Tools/res_reconstruct.ML Tools/ATP/reduce_axiomsN.ML \ |
98 Sum_Type.thy Tools/ATP/reduce_axiomsN.ML Tools/ATP/watcher.ML \ |
101 Tools/ATP/watcher.ML Tools/cnf_funcs.ML Tools/datatype_abs_proofs.ML \ |
99 Tools/Presburger/cooper_dec.ML Tools/Presburger/cooper_proof.ML \ |
102 Tools/datatype_aux.ML Tools/datatype_case.ML Tools/datatype_codegen.ML \ |
100 Tools/Presburger/presburger.ML Tools/Presburger/qelim.ML \ |
|
101 Tools/Presburger/reflected_cooper.ML \ |
|
102 Tools/Presburger/reflected_presburger.ML Tools/cnf_funcs.ML \ |
|
103 Tools/datatype_abs_proofs.ML Tools/datatype_aux.ML \ |
|
104 Tools/datatype_case.ML Tools/datatype_codegen.ML \ |
103 Tools/datatype_hooks.ML Tools/datatype_package.ML \ |
105 Tools/datatype_hooks.ML Tools/datatype_package.ML \ |
104 Tools/datatype_prop.ML Tools/datatype_realizer.ML \ |
106 Tools/datatype_prop.ML Tools/datatype_realizer.ML \ |
105 Tools/datatype_rep_proofs.ML Tools/function_package/auto_term.ML \ |
107 Tools/datatype_rep_proofs.ML Tools/function_package/auto_term.ML \ |
106 Tools/function_package/context_tree.ML \ |
108 Tools/function_package/context_tree.ML \ |
107 Tools/function_package/fundef_common.ML \ |
109 Tools/function_package/fundef_common.ML \ |
|
110 Tools/function_package/fundef_core.ML \ |
108 Tools/function_package/fundef_datatype.ML \ |
111 Tools/function_package/fundef_datatype.ML \ |
109 Tools/function_package/fundef_lib.ML \ |
112 Tools/function_package/fundef_lib.ML \ |
110 Tools/function_package/fundef_package.ML \ |
113 Tools/function_package/fundef_package.ML \ |
111 Tools/function_package/fundef_core.ML \ |
|
112 Tools/function_package/inductive_wrap.ML \ |
114 Tools/function_package/inductive_wrap.ML \ |
113 Tools/function_package/lexicographic_order.ML \ |
115 Tools/function_package/lexicographic_order.ML \ |
114 Tools/function_package/mutual.ML \ |
116 Tools/function_package/mutual.ML \ |
115 Tools/function_package/pattern_split.ML \ |
117 Tools/function_package/pattern_split.ML \ |
116 Tools/function_package/sum_tools.ML \ |
118 Tools/function_package/sum_tools.ML Tools/inductive_codegen.ML \ |
117 Tools/inductive_codegen.ML \ |
|
118 Tools/inductive_package.ML Tools/inductive_realizer.ML Tools/meson.ML \ |
119 Tools/inductive_package.ML Tools/inductive_realizer.ML Tools/meson.ML \ |
119 Tools/numeral_syntax.ML Tools/old_inductive_package.ML \ |
120 Tools/numeral_syntax.ML Tools/old_inductive_package.ML \ |
120 Tools/polyhash.ML Tools/primrec_package.ML Tools/prop_logic.ML \ |
121 Tools/polyhash.ML Tools/primrec_package.ML Tools/prop_logic.ML \ |
121 Tools/recdef_package.ML Tools/recfun_codegen.ML \ |
122 Tools/recdef_package.ML Tools/recfun_codegen.ML \ |
122 Tools/record_package.ML Tools/refute.ML Tools/refute_isar.ML \ |
123 Tools/record_package.ML Tools/refute.ML Tools/refute_isar.ML \ |
123 Tools/res_atp.ML Tools/res_atp_methods.ML Tools/res_atp_provers.ML \ |
124 Tools/res_atp.ML Tools/res_atp_methods.ML Tools/res_atp_provers.ML \ |
124 Tools/res_atpset.ML Tools/res_axioms.ML Tools/res_clause.ML \ |
125 Tools/res_atpset.ML Tools/res_axioms.ML Tools/res_clause.ML \ |
125 Tools/res_hol_clause.ML Tools/rewrite_hol_proof.ML Tools/sat_funcs.ML \ |
126 Tools/res_hol_clause.ML Tools/res_reconstruct.ML \ |
126 Tools/sat_solver.ML Tools/specification_package.ML Tools/split_rule.ML \ |
127 Tools/rewrite_hol_proof.ML Tools/sat_funcs.ML Tools/sat_solver.ML \ |
|
128 Tools/specification_package.ML Tools/split_rule.ML \ |
127 Tools/string_syntax.ML Tools/typecopy_package.ML \ |
129 Tools/string_syntax.ML Tools/typecopy_package.ML \ |
128 Tools/typedef_codegen.ML Tools/typedef_package.ML \ |
130 Tools/typedef_codegen.ML Tools/typedef_package.ML \ |
129 Transitive_Closure.thy Typedef.thy Wellfounded_Recursion.thy \ |
131 Transitive_Closure.thy Typedef.thy Wellfounded_Recursion.thy \ |
130 Wellfounded_Relations.thy arith_data.ML document/root.tex hologic.ML \ |
132 Wellfounded_Relations.thy arith_data.ML document/root.tex hologic.ML \ |
131 simpdata.ML |
133 simpdata.ML |