src/HOL/SMT.thy
changeset 66817 0b12755ccbb2
parent 66559 beb48215cda7
child 67091 1393c2340eec
     1.1 --- a/src/HOL/SMT.thy	Sun Oct 08 22:28:22 2017 +0200
     1.2 +++ b/src/HOL/SMT.thy	Sun Oct 08 22:28:22 2017 +0200
     1.3 @@ -124,8 +124,14 @@
     1.4  lemma int_nat_nneg: "\<forall>i. i \<ge> 0 \<longrightarrow> int (nat i) = i" by simp
     1.5  lemma int_nat_neg: "\<forall>i. i < 0 \<longrightarrow> int (nat i) = 0" by simp
     1.6  
     1.7 -lemmas nat_zero_as_int = transfer_nat_int_numerals(1)
     1.8 -lemmas nat_one_as_int = transfer_nat_int_numerals(2)
     1.9 +lemma nat_zero_as_int:
    1.10 +  "0 = nat 0"
    1.11 +  by simp
    1.12 +
    1.13 +lemma nat_one_as_int:
    1.14 +  "1 = nat 1"
    1.15 +  by simp
    1.16 +
    1.17  lemma nat_numeral_as_int: "numeral = (\<lambda>i. nat (numeral i))" by simp
    1.18  lemma nat_less_as_int: "op < = (\<lambda>a b. int a < int b)" by simp
    1.19  lemma nat_leq_as_int: "op \<le> = (\<lambda>a b. int a \<le> int b)" by simp