src/HOL/Code_Numeral.thy
changeset 55416 dd7992d4a61a
parent 55414 eab03e9cee8a
child 55428 0ab52bf7b5e6
     1.1 --- a/src/HOL/Code_Numeral.thy	Wed Feb 12 08:35:57 2014 +0100
     1.2 +++ b/src/HOL/Code_Numeral.thy	Wed Feb 12 08:35:57 2014 +0100
     1.3 @@ -783,7 +783,7 @@
     1.4    by (rule is_measure_trivial)
     1.5  
     1.6  
     1.7 -subsection {* Inductive represenation of target language naturals *}
     1.8 +subsection {* Inductive representation of target language naturals *}
     1.9  
    1.10  lift_definition Suc :: "natural \<Rightarrow> natural"
    1.11    is Nat.Suc
    1.12 @@ -794,7 +794,7 @@
    1.13  rep_datatype "0::natural" Suc
    1.14    by (transfer, fact nat.induct nat.inject nat.distinct)+
    1.15  
    1.16 -lemma natural_case [case_names nat, cases type: natural]:
    1.17 +lemma natural_cases [case_names nat, cases type: natural]:
    1.18    fixes m :: natural
    1.19    assumes "\<And>n. m = of_nat n \<Longrightarrow> P"
    1.20    shows P
    1.21 @@ -876,7 +876,7 @@
    1.22    by transfer (simp add: fun_eq_iff)
    1.23  
    1.24  lemma [code, code_unfold]:
    1.25 -  "natural_case f g n = (if n = 0 then f else g (n - 1))"
    1.26 +  "case_natural f g n = (if n = 0 then f else g (n - 1))"
    1.27    by (cases n rule: natural.exhaust) (simp_all, simp add: Suc_def)
    1.28  
    1.29  declare natural.recs [code del]