diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/Numeral_Simprocs.thy --- a/src/HOL/Numeral_Simprocs.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/Numeral_Simprocs.thy Wed Aug 22 22:55:41 2012 +0200 @@ -4,16 +4,14 @@ theory Numeral_Simprocs imports Divides -uses - "~~/src/Provers/Arith/assoc_fold.ML" - "~~/src/Provers/Arith/cancel_numerals.ML" - "~~/src/Provers/Arith/combine_numerals.ML" - "~~/src/Provers/Arith/cancel_numeral_factor.ML" - "~~/src/Provers/Arith/extract_common_term.ML" - ("Tools/numeral_simprocs.ML") - ("Tools/nat_numeral_simprocs.ML") begin +ML_file "~~/src/Provers/Arith/assoc_fold.ML" +ML_file "~~/src/Provers/Arith/cancel_numerals.ML" +ML_file "~~/src/Provers/Arith/combine_numerals.ML" +ML_file "~~/src/Provers/Arith/cancel_numeral_factor.ML" +ML_file "~~/src/Provers/Arith/extract_common_term.ML" + lemmas semiring_norm = Let_def arith_simps nat_arith rel_simps if_False if_True @@ -100,7 +98,7 @@ "(k*m) div (k*n) = (if k = (0::nat) then 0 else m div n)" by (simp add: nat_mult_div_cancel1) -use "Tools/numeral_simprocs.ML" +ML_file "Tools/numeral_simprocs.ML" simproc_setup semiring_assoc_fold ("(a::'a::comm_semiring_1_cancel) * b") = @@ -210,7 +208,7 @@ |"(l::'a::field_inverse_zero) / (m * n)") = {* fn phi => Numeral_Simprocs.divide_cancel_factor *} -use "Tools/nat_numeral_simprocs.ML" +ML_file "Tools/nat_numeral_simprocs.ML" simproc_setup nat_combine_numerals ("(i::nat) + j" | "Suc (i + j)") =