src/HOL/Library/Numeral_Type.thy
changeset 64593 50c715579715
parent 62348 9a5f43dac883
child 66886 960509bfd47e
     1.1 --- a/src/HOL/Library/Numeral_Type.thy	Sat Dec 17 15:22:14 2016 +0100
     1.2 +++ b/src/HOL/Library/Numeral_Type.thy	Sat Dec 17 15:22:14 2016 +0100
     1.3 @@ -133,7 +133,7 @@
     1.4  
     1.5  lemma comm_ring_1: "OFCLASS('a, comm_ring_1_class)"
     1.6  apply (intro_classes, unfold definitions)
     1.7 -apply (simp_all add: Rep_simps zmod_simps field_simps)
     1.8 +apply (simp_all add: Rep_simps mod_simps field_simps)
     1.9  done
    1.10  
    1.11  end
    1.12 @@ -147,12 +147,12 @@
    1.13  lemma of_nat_eq: "of_nat k = Abs (int k mod n)"
    1.14  apply (induct k)
    1.15  apply (simp add: zero_def)
    1.16 -apply (simp add: Rep_simps add_def one_def zmod_simps ac_simps)
    1.17 +apply (simp add: Rep_simps add_def one_def mod_simps ac_simps)
    1.18  done
    1.19  
    1.20  lemma of_int_eq: "of_int z = Abs (z mod n)"
    1.21  apply (cases z rule: int_diff_cases)
    1.22 -apply (simp add: Rep_simps of_nat_eq diff_def zmod_simps)
    1.23 +apply (simp add: Rep_simps of_nat_eq diff_def mod_simps)
    1.24  done
    1.25  
    1.26  lemma Rep_numeral: