src/HOL/Code_Numeral.thy
changeset 58377 c6f93b8d2d8e
parent 58306 117ba6cbe414
child 58379 c044539a2bda
     1.1 --- a/src/HOL/Code_Numeral.thy	Thu Sep 18 16:47:40 2014 +0200
     1.2 +++ b/src/HOL/Code_Numeral.thy	Thu Sep 18 16:47:40 2014 +0200
     1.3 @@ -809,22 +809,6 @@
     1.4    shows P
     1.5    using assms by transfer blast
     1.6  
     1.7 -lemma [simp, code]:
     1.8 -  "size_natural = nat_of_natural"
     1.9 -proof (rule ext)
    1.10 -  fix n
    1.11 -  show "size_natural n = nat_of_natural n"
    1.12 -    by (induct n) simp_all
    1.13 -qed
    1.14 -
    1.15 -lemma [simp, code]:
    1.16 -  "size = nat_of_natural"
    1.17 -proof (rule ext)
    1.18 -  fix n
    1.19 -  show "size n = nat_of_natural n"
    1.20 -    by (induct n) simp_all
    1.21 -qed
    1.22 -
    1.23  lemma natural_decr [termination_simp]:
    1.24    "n \<noteq> 0 \<Longrightarrow> nat_of_natural n - Nat.Suc 0 < nat_of_natural n"
    1.25    by transfer simp