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.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)") =
```