proper place for cancel_div_mod.ML (see also ee729dbd1b7f and ec7f10155389);
authorwenzelm
Thu Feb 28 11:40:23 2013 +0100 (2013-02-28)
changeset 5129930b014246e21
parent 51298 ec7f10155389
child 51300 7cdb86c8eb30
proper place for cancel_div_mod.ML (see also ee729dbd1b7f and ec7f10155389);
src/HOL/Divides.thy
src/HOL/Nat_Transfer.thy
     1.1 --- a/src/HOL/Divides.thy	Wed Feb 27 20:36:21 2013 +0100
     1.2 +++ b/src/HOL/Divides.thy	Thu Feb 28 11:40:23 2013 +0100
     1.3 @@ -686,6 +686,8 @@
     1.4  
     1.5  text {* Simproc for cancelling @{const div} and @{const mod} *}
     1.6  
     1.7 +ML_file "~~/src/Provers/Arith/cancel_div_mod.ML"
     1.8 +
     1.9  ML {*
    1.10  structure Cancel_Div_Mod_Nat = Cancel_Div_Mod
    1.11  (
     2.1 --- a/src/HOL/Nat_Transfer.thy	Wed Feb 27 20:36:21 2013 +0100
     2.2 +++ b/src/HOL/Nat_Transfer.thy	Thu Feb 28 11:40:23 2013 +0100
     2.3 @@ -420,8 +420,4 @@
     2.4    return: transfer_int_nat_sum_prod transfer_int_nat_sum_prod2
     2.5    cong: setsum_cong setprod_cong]
     2.6  
     2.7 -
     2.8 -(*belongs to Divides.thy, but slows down dependency discovery*)
     2.9 -ML_file "~~/src/Provers/Arith/cancel_div_mod.ML"
    2.10 -
    2.11  end