src/HOL/Numeral_Simprocs.thy
changeset 48891 c0eafbd55de3
parent 47255 30a1692557b0
child 54249 ce00f2fef556
     1.1 --- a/src/HOL/Numeral_Simprocs.thy	Wed Aug 22 22:47:16 2012 +0200
     1.2 +++ b/src/HOL/Numeral_Simprocs.thy	Wed Aug 22 22:55:41 2012 +0200
     1.3 @@ -4,16 +4,14 @@
     1.4  
     1.5  theory Numeral_Simprocs
     1.6  imports Divides
     1.7 -uses
     1.8 -  "~~/src/Provers/Arith/assoc_fold.ML"
     1.9 -  "~~/src/Provers/Arith/cancel_numerals.ML"
    1.10 -  "~~/src/Provers/Arith/combine_numerals.ML"
    1.11 -  "~~/src/Provers/Arith/cancel_numeral_factor.ML"
    1.12 -  "~~/src/Provers/Arith/extract_common_term.ML"
    1.13 -  ("Tools/numeral_simprocs.ML")
    1.14 -  ("Tools/nat_numeral_simprocs.ML")
    1.15  begin
    1.16  
    1.17 +ML_file "~~/src/Provers/Arith/assoc_fold.ML"
    1.18 +ML_file "~~/src/Provers/Arith/cancel_numerals.ML"
    1.19 +ML_file "~~/src/Provers/Arith/combine_numerals.ML"
    1.20 +ML_file "~~/src/Provers/Arith/cancel_numeral_factor.ML"
    1.21 +ML_file "~~/src/Provers/Arith/extract_common_term.ML"
    1.22 +
    1.23  lemmas semiring_norm =
    1.24    Let_def arith_simps nat_arith rel_simps
    1.25    if_False if_True
    1.26 @@ -100,7 +98,7 @@
    1.27       "(k*m) div (k*n) = (if k = (0::nat) then 0 else m div n)"
    1.28  by (simp add: nat_mult_div_cancel1)
    1.29  
    1.30 -use "Tools/numeral_simprocs.ML"
    1.31 +ML_file "Tools/numeral_simprocs.ML"
    1.32  
    1.33  simproc_setup semiring_assoc_fold
    1.34    ("(a::'a::comm_semiring_1_cancel) * b") =
    1.35 @@ -210,7 +208,7 @@
    1.36    |"(l::'a::field_inverse_zero) / (m * n)") =
    1.37    {* fn phi => Numeral_Simprocs.divide_cancel_factor *}
    1.38  
    1.39 -use "Tools/nat_numeral_simprocs.ML"
    1.40 +ML_file "Tools/nat_numeral_simprocs.ML"
    1.41  
    1.42  simproc_setup nat_combine_numerals
    1.43    ("(i::nat) + j" | "Suc (i + j)") =