src/HOL/Code_Numeral.thy
changeset 34917 51829fe604a7
parent 34898 62d70417f8ce
parent 34915 7894c7dab132
child 34944 970e1466028d
     1.1 --- a/src/HOL/Code_Numeral.thy	Fri Jan 15 08:27:21 2010 +0100
     1.2 +++ b/src/HOL/Code_Numeral.thy	Fri Jan 15 14:43:00 2010 +0100
     1.3 @@ -83,7 +83,7 @@
     1.4      then have "\<And>n. P (of_nat n) \<Longrightarrow> P (Suc_code_numeral (of_nat n))" .
     1.5      then have step: "\<And>n. P (of_nat n) \<Longrightarrow> P (of_nat (Suc n))" by simp
     1.6    from init step have "P (of_nat (nat_of k))"
     1.7 -    by (induct "nat_of k") simp_all
     1.8 +    by (induct ("nat_of k")) simp_all
     1.9    then show "P k" by simp
    1.10  qed simp_all
    1.11  
    1.12 @@ -100,7 +100,7 @@
    1.13    fix k
    1.14    have "code_numeral_size k = nat_size (nat_of k)"
    1.15      by (induct k rule: code_numeral.induct) (simp_all del: zero_code_numeral_def Suc_code_numeral_def, simp_all)
    1.16 -  also have "nat_size (nat_of k) = nat_of k" by (induct "nat_of k") simp_all
    1.17 +  also have "nat_size (nat_of k) = nat_of k" by (induct ("nat_of k")) simp_all
    1.18    finally show "code_numeral_size k = nat_of k" .
    1.19  qed
    1.20