src/HOL/Int.thy
changeset 61694 6571c78c9667
parent 61649 268d88ec9087
child 61738 c4f6031f1310
     1.1 --- a/src/HOL/Int.thy	Tue Nov 17 12:01:19 2015 +0100
     1.2 +++ b/src/HOL/Int.thy	Tue Nov 17 12:32:08 2015 +0000
     1.3 @@ -524,9 +524,6 @@
     1.4  lemma zadd_int_left: "int m + (int n + z) = int (m + n) + z"
     1.5  by simp
     1.6  
     1.7 -lemma int_Suc0_eq_1: "int (Suc 0) = 1"
     1.8 -by simp
     1.9 -
    1.10  text\<open>This version is proved for all ordered rings, not just integers!
    1.11        It is proved here because attribute @{text arith_split} is not available
    1.12        in theory @{text Rings}.
    1.13 @@ -843,7 +840,6 @@
    1.14  
    1.15  lemmas zle_int = of_nat_le_iff [where 'a=int]
    1.16  lemmas int_int_eq = of_nat_eq_iff [where 'a=int]
    1.17 -lemmas numeral_1_eq_1 = numeral_One
    1.18  
    1.19  subsection \<open>Setting up simplification procedures\<close>
    1.20  
    1.21 @@ -1678,7 +1674,6 @@
    1.22  lemmas inj_int = inj_of_nat [where 'a=int]
    1.23  lemmas zadd_int = of_nat_add [where 'a=int, symmetric]
    1.24  lemmas int_mult = of_nat_mult [where 'a=int]
    1.25 -lemmas zmult_int = of_nat_mult [where 'a=int, symmetric]
    1.26  lemmas int_eq_0_conv = of_nat_eq_0_iff [where 'a=int and m="n"] for n
    1.27  lemmas zless_int = of_nat_less_iff [where 'a=int]
    1.28  lemmas int_less_0_conv = of_nat_less_0_iff [where 'a=int and m="k"] for k