src/HOL/IsaMakefile
changeset 15481 fc075ae929e4
parent 15418 e28853da5df5
child 15513 1a2aedd20d37
equal deleted inserted replaced
15480:cb3612cc41a3 15481:fc075ae929e4
    72   $(SRC)/Provers/Arith/extract_common_term.ML \
    72   $(SRC)/Provers/Arith/extract_common_term.ML \
    73   $(SRC)/Provers/Arith/cancel_div_mod.ML \
    73   $(SRC)/Provers/Arith/cancel_div_mod.ML \
    74   $(SRC)/Provers/Arith/fast_lin_arith.ML $(SRC)/Provers/blast.ML \
    74   $(SRC)/Provers/Arith/fast_lin_arith.ML $(SRC)/Provers/blast.ML \
    75   $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \
    75   $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \
    76   $(SRC)/Provers/hypsubst.ML $(SRC)/Provers/induct_method.ML \
    76   $(SRC)/Provers/hypsubst.ML $(SRC)/Provers/induct_method.ML \
    77   $(SRC)/Provers/make_elim.ML $(SRC)/Provers/order.ML \
    77   $(SRC)/Provers/make_elim.ML $(SRC)/Provers/order.ML $(SRC)/Provers/quasi.ML\
    78   $(SRC)/Provers/quasi.ML \
       
    79   $(SRC)/Provers/simplifier.ML $(SRC)/Provers/splitter.ML \
    78   $(SRC)/Provers/simplifier.ML $(SRC)/Provers/splitter.ML \
    80   $(SRC)/Provers/trancl.ML \
    79   $(SRC)/Provers/trancl.ML \
    81   $(SRC)/TFL/dcterm.ML $(SRC)/TFL/post.ML $(SRC)/TFL/rules.ML \
    80   $(SRC)/TFL/dcterm.ML $(SRC)/TFL/post.ML $(SRC)/TFL/rules.ML \
    82   $(SRC)/TFL/tfl.ML $(SRC)/TFL/thms.ML $(SRC)/TFL/thry.ML \
    81   $(SRC)/TFL/tfl.ML $(SRC)/TFL/thms.ML $(SRC)/TFL/thry.ML \
    83   $(SRC)/TFL/usyntax.ML $(SRC)/TFL/utils.ML \
    82   $(SRC)/TFL/usyntax.ML $(SRC)/TFL/utils.ML \
       
    83   $(SRC)/Provers/eqsubst.ML\
       
    84   eqrule_HOL_data.ML\
    84   Datatype.thy Datatype_Universe.thy \
    85   Datatype.thy Datatype_Universe.thy \
    85   Divides.thy Equiv_Relations.thy Extraction.thy Finite_Set.ML Finite_Set.thy \
    86   Divides.thy Equiv_Relations.thy Extraction.thy Finite_Set.ML Finite_Set.thy \
    86   Fun.thy Gfp.thy Hilbert_Choice.thy HOL.ML \
    87   Fun.thy Gfp.thy Hilbert_Choice.thy HOL.ML \
    87   HOL.thy Inductive.thy Infinite_Set.thy Integ/Numeral.thy \
    88   HOL.thy Inductive.thy Infinite_Set.thy Integ/Numeral.thy \
    88   Integ/cooper_dec.ML Integ/cooper_proof.ML \
    89   Integ/cooper_dec.ML Integ/cooper_proof.ML \