src/HOL/Arith_Tools.thy
changeset 28952 15a4b2cf8c34
parent 28402 09e4aa3ddc25
child 29012 9140227dc8c5
equal deleted inserted replaced
28948:1860f016886d 28952:15a4b2cf8c34
     9 theory Arith_Tools
     9 theory Arith_Tools
    10 imports NatBin
    10 imports NatBin
    11 uses
    11 uses
    12   "~~/src/Provers/Arith/cancel_numeral_factor.ML"
    12   "~~/src/Provers/Arith/cancel_numeral_factor.ML"
    13   "~~/src/Provers/Arith/extract_common_term.ML"
    13   "~~/src/Provers/Arith/extract_common_term.ML"
    14   "int_factor_simprocs.ML"
    14   "Tools/int_factor_simprocs.ML"
    15   "nat_simprocs.ML"
    15   "Tools/nat_simprocs.ML"
    16   "Tools/Qelim/qelim.ML"
    16   "Tools/Qelim/qelim.ML"
    17 begin
    17 begin
    18 
    18 
    19 subsection {* Simprocs for the Naturals *}
    19 subsection {* Simprocs for the Naturals *}
    20 
    20