79 $(SRC)/Provers/Arith/extract_common_term.ML \ |
79 $(SRC)/Provers/Arith/extract_common_term.ML \ |
80 $(SRC)/Provers/Arith/fast_lin_arith.ML \ |
80 $(SRC)/Provers/Arith/fast_lin_arith.ML \ |
81 $(SRC)/Tools/IsaPlanner/isand.ML $(SRC)/Tools/IsaPlanner/rw_inst.ML \ |
81 $(SRC)/Tools/IsaPlanner/isand.ML $(SRC)/Tools/IsaPlanner/rw_inst.ML \ |
82 $(SRC)/Tools/IsaPlanner/rw_tools.ML \ |
82 $(SRC)/Tools/IsaPlanner/rw_tools.ML \ |
83 $(SRC)/Tools/IsaPlanner/zipper.ML $(SRC)/Tools/induct.ML \ |
83 $(SRC)/Tools/IsaPlanner/zipper.ML $(SRC)/Tools/induct.ML \ |
84 $(SRC)/Provers/blast.ML $(SRC)/Provers/clasimp.ML \ |
84 $(SRC)/Tools/induct_tacs.ML $(SRC)/Provers/blast.ML \ |
85 $(SRC)/Provers/classical.ML $(SRC)/Provers/eqsubst.ML \ |
85 $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \ |
86 $(SRC)/Provers/hypsubst.ML $(SRC)/Provers/order.ML \ |
86 $(SRC)/Provers/eqsubst.ML $(SRC)/Provers/hypsubst.ML \ |
87 $(SRC)/Provers/project_rule.ML $(SRC)/Provers/quantifier1.ML \ |
87 $(SRC)/Provers/order.ML $(SRC)/Provers/project_rule.ML \ |
88 $(SRC)/Provers/quasi.ML $(SRC)/Provers/splitter.ML \ |
88 $(SRC)/Provers/quantifier1.ML $(SRC)/Provers/quasi.ML \ |
89 $(SRC)/Provers/trancl.ML $(SRC)/Tools/Metis/metis.ML \ |
89 $(SRC)/Provers/splitter.ML $(SRC)/Provers/trancl.ML \ |
90 $(SRC)/Tools/code/code_funcgr.ML $(SRC)/Tools/code/code_name.ML \ |
90 $(SRC)/Tools/Metis/metis.ML $(SRC)/Tools/code/code_funcgr.ML \ |
91 $(SRC)/Tools/code/code_target.ML $(SRC)/Tools/code/code_thingol.ML \ |
91 $(SRC)/Tools/code/code_name.ML $(SRC)/Tools/code/code_target.ML \ |
92 $(SRC)/Tools/nbe.ML $(SRC)/Tools/atomize_elim.ML \ |
92 $(SRC)/Tools/code/code_thingol.ML $(SRC)/Tools/nbe.ML \ |
93 $(SRC)/Tools/random_word.ML $(SRC)/Tools/rat.ML \ |
93 $(SRC)/Tools/atomize_elim.ML $(SRC)/Tools/random_word.ML \ |
94 Tools/TFL/casesplit.ML ATP_Linkup.thy Arith_Tools.thy Code_Setup.thy \ |
94 $(SRC)/Tools/rat.ML Tools/TFL/casesplit.ML ATP_Linkup.thy \ |
95 Datatype.thy Divides.thy Equiv_Relations.thy Extraction.thy \ |
95 Arith_Tools.thy Code_Setup.thy Datatype.thy Divides.thy \ |
96 Finite_Set.thy Fun.thy FunDef.thy HOL.thy Hilbert_Choice.thy \ |
96 Equiv_Relations.thy Extraction.thy Finite_Set.thy Fun.thy FunDef.thy \ |
97 Inductive.thy Int.thy IntDiv.thy Lattices.thy List.thy Main.thy \ |
97 HOL.thy Hilbert_Choice.thy Inductive.thy Int.thy IntDiv.thy \ |
98 Map.thy Nat.thy NatBin.thy OrderedGroup.thy Orderings.thy Power.thy \ |
98 Lattices.thy List.thy Main.thy Map.thy Nat.thy NatBin.thy \ |
99 Predicate.thy Product_Type.thy ROOT.ML Recdef.thy Record.thy \ |
99 OrderedGroup.thy Orderings.thy Power.thy Predicate.thy \ |
100 Refute.thy Relation.thy Relation_Power.thy Ring_and_Field.thy \ |
100 Product_Type.thy ROOT.ML Recdef.thy Record.thy Refute.thy \ |
101 SAT.thy Set.thy SetInterval.thy Sum_Type.thy Groebner_Basis.thy \ |
101 Relation.thy Relation_Power.thy Ring_and_Field.thy SAT.thy Set.thy \ |
102 Tools/watcher.ML Tools/Groebner_Basis/groebner.ML \ |
102 SetInterval.thy Sum_Type.thy Groebner_Basis.thy Tools/watcher.ML \ |
103 Tools/Groebner_Basis/misc.ML Tools/Groebner_Basis/normalizer.ML \ |
103 Tools/Groebner_Basis/groebner.ML Tools/Groebner_Basis/misc.ML \ |
|
104 Tools/Groebner_Basis/normalizer.ML \ |
104 Tools/Groebner_Basis/normalizer_data.ML Tools/Qelim/cooper.ML \ |
105 Tools/Groebner_Basis/normalizer_data.ML Tools/Qelim/cooper.ML \ |
105 Tools/Qelim/langford_data.ML Tools/Qelim/langford.ML \ |
106 Tools/Qelim/langford_data.ML Tools/Qelim/langford.ML \ |
106 Tools/Qelim/cooper_data.ML Tools/Qelim/ferrante_rackoff.ML \ |
107 Tools/Qelim/cooper_data.ML Tools/Qelim/ferrante_rackoff.ML \ |
107 Tools/Qelim/ferrante_rackoff_data.ML Tools/Qelim/generated_cooper.ML \ |
108 Tools/Qelim/ferrante_rackoff_data.ML Tools/Qelim/generated_cooper.ML \ |
108 Tools/Qelim/presburger.ML Tools/Qelim/qelim.ML Tools/TFL/dcterm.ML \ |
109 Tools/Qelim/presburger.ML Tools/Qelim/qelim.ML Tools/TFL/dcterm.ML \ |
123 Tools/function_package/inductive_wrap.ML \ |
124 Tools/function_package/inductive_wrap.ML \ |
124 Tools/function_package/lexicographic_order.ML \ |
125 Tools/function_package/lexicographic_order.ML \ |
125 Tools/function_package/measure_functions.ML \ |
126 Tools/function_package/measure_functions.ML \ |
126 Tools/function_package/mutual.ML \ |
127 Tools/function_package/mutual.ML \ |
127 Tools/function_package/pattern_split.ML \ |
128 Tools/function_package/pattern_split.ML \ |
128 Tools/function_package/size.ML Tools/induct_tacs.ML \ |
129 Tools/function_package/size.ML Tools/inductive_codegen.ML \ |
129 Tools/inductive_codegen.ML Tools/inductive_package.ML \ |
130 Tools/inductive_package.ML Tools/inductive_realizer.ML \ |
130 Tools/inductive_realizer.ML Tools/inductive_set_package.ML \ |
131 Tools/inductive_set_package.ML Tools/lin_arith.ML Tools/meson.ML \ |
131 Tools/lin_arith.ML Tools/meson.ML Tools/metis_tools.ML \ |
132 Tools/metis_tools.ML Tools/numeral.ML Tools/numeral_syntax.ML \ |
132 Tools/numeral.ML Tools/numeral_syntax.ML \ |
|
133 Tools/old_primrec_package.ML Tools/polyhash.ML \ |
133 Tools/old_primrec_package.ML Tools/polyhash.ML \ |
134 Tools/primrec_package.ML Tools/prop_logic.ML Tools/recdef_package.ML \ |
134 Tools/primrec_package.ML Tools/prop_logic.ML Tools/recdef_package.ML \ |
135 Tools/recfun_codegen.ML Tools/record_package.ML Tools/refute.ML \ |
135 Tools/recfun_codegen.ML Tools/record_package.ML Tools/refute.ML \ |
136 Tools/refute_isar.ML Tools/res_atp.ML Tools/res_atp_methods.ML \ |
136 Tools/refute_isar.ML Tools/res_atp.ML Tools/res_atp_methods.ML \ |
137 Tools/res_atp_provers.ML Tools/res_axioms.ML Tools/res_clause.ML \ |
137 Tools/res_atp_provers.ML Tools/res_axioms.ML Tools/res_clause.ML \ |