Pure/General/graph.ML:functor GraphFun(Key: KEY): GRAPH = Pure/General/heap.ML:functor HeapFun(type elem val ord: elem * elem -> order): HEAP = Pure/General/table.ML:functor TableFun(Key: KEY): TABLE = Pure/Isar/proof_data.ML:functor ProofDataFun(Args: PROOF_DATA_ARGS): PROOF_DATA = Pure/theory_data.ML:functor TheoryDataFun(Args: THEORY_DATA_ARGS): THEORY_DATA = Sequents/modal.ML:functor Modal_ProverFun (Modal_Rule: MODAL_PROVER_RULE) : MODAL_PROVER = (** proof techniques **) Provers/blast.ML:functor BlastFun(Data: BLAST_DATA) : BLAST = Provers/clasimp.ML:functor ClasimpFun(Data: CLASIMP_DATA): CLASIMP = Provers/classical.ML:functor ClassicalFun(Data: CLASSICAL_DATA): CLASSICAL = Provers/hypsubst.ML:functor HypsubstFun(Data: HYPSUBST_DATA): HYPSUBST = Provers/ind.ML:functor InductionFun(Ind_Data: IND_DATA):IND = Provers/induct_method.ML:functor InductMethodFun(Data: INDUCT_METHOD_DATA): INDUCT_METHOD = Provers/make_elim.ML:functor Make_Elim_Fun(Data: MAKE_ELIM_DATA) = Provers/order.ML:functor Trans_Tac_Fun (Less: LESS_ARITH): TRANS_TAC = Provers/quantifier1.ML:functor Quantifier1Fun(Data: QUANTIFIER1_DATA): QUANTIFIER1 = Provers/simp.ML:functor SimpFun (Simp_data: SIMP_DATA) : SIMP = Provers/splitter.ML:functor SplitterFun(Data: SPLITTER_DATA): SPLITTER = Provers/typedsimp.ML:functor TSimpFun (TSimp_data: TSIMP_DATA) : TSIMP = (** arithmetic proof techniques **) mostly used in HOL/arith_data.ML, HOL/Integ/int_arith1.ML HOL/Integ/int_factor_simprocs.ML, HOL/Integ/nat_simprocs.ML, Provers/Arith/abel_cancel.ML:functor Abel_Cancel (Data: ABEL_CANCEL) = Provers/Arith/abstract_numerals.ML:functor AbstractNumeralsFun(Data: ABSTRACT_NUMERALS_DATA): Provers/Arith/assoc_fold.ML:functor Assoc_Fold (Data: ASSOC_FOLD_DATA) = Provers/Arith/cancel_div_mod.ML:functor CancelDivModFun(Data: CANCEL_DIV_MOD_DATA): CANCEL_DIV_MOD = Provers/Arith/cancel_factor.ML:functor CancelFactorFun(Data: CANCEL_FACTOR_DATA): CANCEL_FACTOR = Provers/Arith/cancel_numeral_factor.ML:functor CancelNumeralFactorFun(Data: CANCEL_NUMERAL_FACTOR_DATA): Provers/Arith/cancel_numerals.ML:functor CancelNumeralsFun(Data: CANCEL_NUMERALS_DATA): Provers/Arith/cancel_sums.ML:functor CancelSumsFun(Data: CANCEL_SUMS_DATA): CANCEL_SUMS = Provers/Arith/combine_numerals.ML:functor CombineNumeralsFun(Data: COMBINE_NUMERALS_DATA): Provers/Arith/extract_common_term.ML:functor ExtractCommonTermFun(Data: EXTRACT_COMMON_TERM_DATA): Provers/Arith/fast_lin_arith.ML:functor Fast_Lin_Arith(structure LA_Logic:LIN_ARITH_LOGIC