src/HOL/Code_Numeral.thy
changeset 56846 9df717fef2bb
parent 55945 e96383acecf9
child 57512 cc97b347b301
     1.1 --- a/src/HOL/Code_Numeral.thy	Sun May 04 16:17:53 2014 +0200
     1.2 +++ b/src/HOL/Code_Numeral.thy	Sun May 04 18:14:58 2014 +0200
     1.3 @@ -810,10 +810,10 @@
     1.4    using assms by transfer blast
     1.5  
     1.6  lemma [simp, code]:
     1.7 -  "natural_size = nat_of_natural"
     1.8 +  "size_natural = nat_of_natural"
     1.9  proof (rule ext)
    1.10    fix n
    1.11 -  show "natural_size n = nat_of_natural n"
    1.12 +  show "size_natural n = nat_of_natural n"
    1.13      by (induct n) simp_all
    1.14  qed
    1.15