src/HOL/IsaMakefile
changeset 21753 83b6cc133b28
parent 21669 c68717c16013
child 21777 a535be528d3a
equal deleted inserted replaced
21752:5b7644879373 21753:83b6cc133b28
    68   $(SRC)/Provers/Arith/cancel_numeral_factor.ML					\
    68   $(SRC)/Provers/Arith/cancel_numeral_factor.ML					\
    69   $(SRC)/Provers/Arith/cancel_numerals.ML					\
    69   $(SRC)/Provers/Arith/cancel_numerals.ML					\
    70   $(SRC)/Provers/Arith/cancel_sums.ML						\
    70   $(SRC)/Provers/Arith/cancel_sums.ML						\
    71   $(SRC)/Provers/Arith/combine_numerals.ML					\
    71   $(SRC)/Provers/Arith/combine_numerals.ML					\
    72   $(SRC)/Provers/Arith/extract_common_term.ML					\
    72   $(SRC)/Provers/Arith/extract_common_term.ML					\
    73   $(SRC)/Provers/Arith/fast_lin_arith.ML $(SRC)/Provers/blast.ML		\
    73   $(SRC)/Provers/Arith/fast_lin_arith.ML					\
       
    74   $(SRC)/Provers/IsaPlanner/isand.ML						\
       
    75   $(SRC)/Provers/IsaPlanner/rw_inst.ML						\
       
    76   $(SRC)/Provers/IsaPlanner/rw_tools.ML						\
       
    77   $(SRC)/Provers/IsaPlanner/zipper.ML $(SRC)/Provers/blast.ML			\
    74   $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML				\
    78   $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML				\
    75   $(SRC)/Provers/IsaPlanner/zipper.ML \
       
    76   $(SRC)/Provers/IsaPlanner/isand.ML \
       
    77   $(SRC)/Provers/IsaPlanner/rw_tools.ML	\
       
    78   $(SRC)/Provers/IsaPlanner/rw_inst.ML \
       
    79   $(SRC)/Provers/eqsubst.ML $(SRC)/Provers/hypsubst.ML				\
    79   $(SRC)/Provers/eqsubst.ML $(SRC)/Provers/hypsubst.ML				\
    80   $(SRC)/Provers/induct_method.ML $(SRC)/Provers/order.ML			\
    80   $(SRC)/Provers/induct_method.ML $(SRC)/Provers/order.ML			\
    81   $(SRC)/Provers/project_rule.ML $(SRC)/Provers/quantifier1.ML			\
    81   $(SRC)/Provers/project_rule.ML $(SRC)/Provers/quantifier1.ML			\
    82   $(SRC)/Provers/quasi.ML $(SRC)/Provers/splitter.ML $(SRC)/Provers/trancl.ML	\
    82   $(SRC)/Provers/quasi.ML $(SRC)/Provers/splitter.ML				\
    83   $(SRC)/TFL/casesplit.ML $(SRC)/TFL/dcterm.ML $(SRC)/TFL/post.ML		\
    83   $(SRC)/Provers/trancl.ML $(SRC)/TFL/casesplit.ML $(SRC)/TFL/dcterm.ML		\
    84   $(SRC)/TFL/rules.ML $(SRC)/TFL/tfl.ML $(SRC)/TFL/thms.ML			\
    84   $(SRC)/TFL/post.ML $(SRC)/TFL/rules.ML $(SRC)/TFL/tfl.ML			\
    85   $(SRC)/TFL/thry.ML $(SRC)/TFL/usyntax.ML $(SRC)/TFL/utils.ML			\
    85   $(SRC)/TFL/thms.ML $(SRC)/TFL/thry.ML $(SRC)/TFL/usyntax.ML			\
    86   Tools/res_atpset.ML \
    86   $(SRC)/TFL/utils.ML ATP_Linkup.thy Accessible_Part.thy			\
    87   Code_Generator.thy Datatype.thy Divides.thy					\
    87   Code_Generator.thy Datatype.thy Divides.thy Equiv_Relations.thy		\
    88   Equiv_Relations.thy Extraction.thy Finite_Set.thy				\
    88   Extraction.thy Finite_Set.thy FixedPoint.thy Fun.thy FunDef.thy HOL.ML	\
    89   FixedPoint.thy Fun.thy HOL.ML HOL.thy Hilbert_Choice.thy Inductive.thy	\
    89   HOL.thy Hilbert_Choice.thy Inductive.thy Integ/IntArith.thy			\
    90   Integ/IntArith.thy Integ/IntDef.thy Integ/IntDiv.thy				\
    90   Integ/IntDef.thy Integ/IntDiv.thy Integ/NatBin.thy				\
    91   Integ/NatBin.thy Integ/NatSimprocs.thy Integ/Numeral.thy			\
    91   Integ/NatSimprocs.thy Integ/Numeral.thy Integ/Presburger.thy			\
    92   Integ/Presburger.thy Integ/cooper_dec.ML			\
    92   Integ/cooper_dec.ML Integ/cooper_proof.ML Integ/int_arith1.ML			\
    93   Integ/cooper_proof.ML Integ/reflected_presburger.ML				\
    93   Integ/int_factor_simprocs.ML Integ/nat_simprocs.ML Integ/presburger.ML	\
    94   Integ/reflected_cooper.ML Integ/int_arith1.ML Integ/int_factor_simprocs.ML	\
    94   Integ/qelim.ML Integ/reflected_cooper.ML Integ/reflected_presburger.ML	\
    95   Integ/nat_simprocs.ML Integ/presburger.ML Integ/qelim.ML LOrder.thy		\
    95   LOrder.thy Lattices.thy List.thy Main.thy Map.thy Nat.ML Nat.thy		\
    96   Lattices.thy List.thy Main.thy Map.thy Nat.thy Nat.ML OrderedGroup.ML		\
    96   OrderedGroup.ML OrderedGroup.thy Orderings.thy Power.thy PreList.thy		\
    97   OrderedGroup.thy Orderings.thy Power.thy PreList.thy Product_Type.thy		\
    97   Product_Type.thy ROOT.ML Recdef.thy Record.thy Refute.thy Relation.thy	\
    98   ROOT.ML Recdef.thy Record.thy Refute.thy			\
    98   Relation_Power.thy Ring_and_Field.thy SAT.thy Set.thy SetInterval.thy		\
    99   Relation.thy Relation_Power.thy Ring_and_Field.thy SAT.thy 			\
    99   Sum_Type.thy Tools/ATP/AtpCommunication.ML Tools/ATP/reduce_axiomsN.ML	\
   100   Set.thy SetInterval.thy Sum_Type.thy Tools/ATP/AtpCommunication.ML		\
   100   Tools/ATP/watcher.ML Tools/cnf_funcs.ML Tools/datatype_abs_proofs.ML		\
   101   Tools/ATP/reduce_axiomsN.ML Tools/ATP/watcher.ML 					\
   101   Tools/datatype_aux.ML Tools/datatype_codegen.ML				\
   102   Tools/cnf_funcs.ML					\
   102   Tools/datatype_hooks.ML Tools/datatype_package.ML				\
   103   Tools/datatype_abs_proofs.ML Tools/datatype_aux.ML				\
       
   104   Tools/datatype_codegen.ML Tools/datatype_hooks.ML Tools/datatype_package.ML	\
       
   105   Tools/datatype_prop.ML Tools/datatype_realizer.ML				\
   103   Tools/datatype_prop.ML Tools/datatype_realizer.ML				\
   106   Tools/datatype_rep_proofs.ML Tools/inductive_codegen.ML			\
   104   Tools/datatype_rep_proofs.ML Tools/function_package/auto_term.ML		\
   107   Tools/inductive_package.ML Tools/old_inductive_package.ML Tools/inductive_realizer.ML Tools/meson.ML		\
   105   Tools/function_package/context_tree.ML					\
   108   Tools/numeral_syntax.ML Tools/primrec_package.ML Tools/prop_logic.ML		\
   106   Tools/function_package/fundef_common.ML					\
   109   Tools/polyhash.ML \
   107   Tools/function_package/fundef_datatype.ML					\
       
   108   Tools/function_package/fundef_lib.ML						\
       
   109   Tools/function_package/fundef_package.ML					\
       
   110   Tools/function_package/fundef_prep.ML						\
       
   111   Tools/function_package/fundef_proof.ML					\
       
   112   Tools/function_package/inductive_wrap.ML					\
       
   113   Tools/function_package/lexicographic_order.ML					\
       
   114   Tools/function_package/mutual.ML						\
       
   115   Tools/function_package/pattern_split.ML					\
       
   116   Tools/function_package/sum_tools.ML						\
       
   117   Tools/function_package/termination.ML Tools/inductive_codegen.ML		\
       
   118   Tools/inductive_package.ML Tools/inductive_realizer.ML Tools/meson.ML		\
       
   119   Tools/numeral_syntax.ML Tools/old_inductive_package.ML			\
       
   120   Tools/polyhash.ML Tools/primrec_package.ML Tools/prop_logic.ML		\
   110   Tools/recdef_package.ML Tools/recfun_codegen.ML				\
   121   Tools/recdef_package.ML Tools/recfun_codegen.ML				\
   111   Tools/record_package.ML Tools/refute.ML		\
   122   Tools/record_package.ML Tools/refute.ML Tools/refute_isar.ML			\
   112   Tools/refute_isar.ML Tools/res_atp.ML Tools/res_axioms.ML			\
   123   Tools/res_atp.ML Tools/res_atp_methods.ML Tools/res_atp_provers.ML		\
   113   Tools/res_clause.ML Tools/rewrite_hol_proof.ML	\
   124   Tools/res_atpset.ML Tools/res_axioms.ML Tools/res_clause.ML			\
   114   Tools/sat_funcs.ML					\
   125   Tools/res_hol_clause.ML Tools/rewrite_hol_proof.ML Tools/sat_funcs.ML		\
   115   Tools/sat_solver.ML Tools/specification_package.ML Tools/split_rule.ML	\
   126   Tools/sat_solver.ML Tools/specification_package.ML Tools/split_rule.ML	\
   116   Tools/typecopy_package.ML	\
   127   Tools/string_syntax.ML Tools/typecopy_package.ML				\
   117   Tools/typedef_package.ML Tools/typedef_codegen.ML	\
   128   Tools/typedef_codegen.ML Tools/typedef_package.ML				\
   118   Transitive_Closure.thy Typedef.thy Wellfounded_Recursion.thy		\
   129   Transitive_Closure.thy Typedef.thy Wellfounded_Recursion.thy			\
   119   Wellfounded_Relations.thy arith_data.ML			\
   130   Wellfounded_Relations.thy arith_data.ML document/root.tex hologic.ML		\
   120   document/root.tex hologic.ML simpdata.ML ATP_Linkup.thy \
   131   simpdata.ML
   121   Tools/res_atp_provers.ML Tools/res_atp_methods.ML	\
       
   122   Tools/res_hol_clause.ML	\
       
   123   Tools/function_package/sum_tools.ML 	\
       
   124   Tools/function_package/fundef_common.ML 	\
       
   125   Tools/function_package/fundef_lib.ML 	\
       
   126   Tools/function_package/inductive_wrap.ML 	\
       
   127   Tools/function_package/context_tree.ML 	\
       
   128   Tools/function_package/fundef_prep.ML 	\
       
   129   Tools/function_package/fundef_proof.ML 	\
       
   130   Tools/function_package/termination.ML 	\
       
   131   Tools/function_package/pattern_split.ML 	\
       
   132   Tools/function_package/mutual.ML 	\
       
   133   Tools/function_package/fundef_package.ML 	\
       
   134   Tools/function_package/auto_term.ML 	\
       
   135   Tools/function_package/lexicographic_order.ML 	\
       
   136   Tools/function_package/fundef_datatype.ML 	\
       
   137   FunDef.thy Accessible_Part.thy 
       
   138 	@$(ISATOOL) usedir $(HOL_USEDIR_OPTIONS) -b -g true $(OUT)/Pure HOL
   132 	@$(ISATOOL) usedir $(HOL_USEDIR_OPTIONS) -b -g true $(OUT)/Pure HOL
   139 
   133 
   140 
   134 
   141 ## HOL-Complex-HahnBanach
   135 ## HOL-Complex-HahnBanach
   142 
   136