src/HOL/Tools/nat_numeral_simprocs.ML
changeset 35050 9f841f20dca6
parent 34974 18b41bba42b5
child 35064 1bdef0c013d3
     1.1 --- a/src/HOL/Tools/nat_numeral_simprocs.ML	Mon Feb 08 17:12:32 2010 +0100
     1.2 +++ b/src/HOL/Tools/nat_numeral_simprocs.ML	Mon Feb 08 17:12:38 2010 +0100
     1.3 @@ -124,7 +124,7 @@
     1.4  
     1.5  
     1.6  (*Simplify 1*n and n*1 to n*)
     1.7 -val add_0s  = map rename_numerals [@{thm add_0}, @{thm add_0_right}];
     1.8 +val add_0s  = map rename_numerals [@{thm add_0}, @{thm Nat.add_0_right}];
     1.9  val mult_1s = map rename_numerals [@{thm nat_mult_1}, @{thm nat_mult_1_right}];
    1.10  
    1.11  (*Final simplification: cancel + and *; replace Numeral0 by 0 and Numeral1 by 1*)
    1.12 @@ -136,7 +136,7 @@
    1.13  
    1.14  val simplify_meta_eq =
    1.15      Arith_Data.simplify_meta_eq
    1.16 -        ([@{thm nat_numeral_0_eq_0}, @{thm numeral_1_eq_Suc_0}, @{thm add_0}, @{thm add_0_right},
    1.17 +        ([@{thm nat_numeral_0_eq_0}, @{thm numeral_1_eq_Suc_0}, @{thm add_0}, @{thm Nat.add_0_right},
    1.18            @{thm mult_0}, @{thm mult_0_right}, @{thm mult_1}, @{thm mult_1_right}] @ contra_rules);
    1.19  
    1.20  
    1.21 @@ -290,8 +290,8 @@
    1.22  structure DvdCancelNumeralFactor = CancelNumeralFactorFun
    1.23   (open CancelNumeralFactorCommon
    1.24    val prove_conv = Arith_Data.prove_conv
    1.25 -  val mk_bal   = HOLogic.mk_binrel @{const_name Ring_and_Field.dvd}
    1.26 -  val dest_bal = HOLogic.dest_bin @{const_name Ring_and_Field.dvd} HOLogic.natT
    1.27 +  val mk_bal   = HOLogic.mk_binrel @{const_name Rings.dvd}
    1.28 +  val dest_bal = HOLogic.dest_bin @{const_name Rings.dvd} HOLogic.natT
    1.29    val cancel = @{thm nat_mult_dvd_cancel1} RS trans
    1.30    val neg_exchanges = false
    1.31  )
    1.32 @@ -411,8 +411,8 @@
    1.33  structure DvdCancelFactor = ExtractCommonTermFun
    1.34   (open CancelFactorCommon
    1.35    val prove_conv = Arith_Data.prove_conv
    1.36 -  val mk_bal   = HOLogic.mk_binrel @{const_name Ring_and_Field.dvd}
    1.37 -  val dest_bal = HOLogic.dest_bin @{const_name Ring_and_Field.dvd} HOLogic.natT
    1.38 +  val mk_bal   = HOLogic.mk_binrel @{const_name Rings.dvd}
    1.39 +  val dest_bal = HOLogic.dest_bin @{const_name Rings.dvd} HOLogic.natT
    1.40    fun simp_conv _ _ = SOME @{thm nat_mult_dvd_cancel_disj}
    1.41  );
    1.42