src/HOL/String.thy
changeset 55416 dd7992d4a61a
parent 55015 e33c5bd729ff
child 55428 0ab52bf7b5e6
     1.1 --- a/src/HOL/String.thy	Wed Feb 12 08:35:57 2014 +0100
     1.2 +++ b/src/HOL/String.thy	Wed Feb 12 08:35:57 2014 +0100
     1.3 @@ -286,13 +286,13 @@
     1.4  
     1.5  code_datatype Char -- {* drop case certificate for char *}
     1.6  
     1.7 -lemma char_case_code [code]:
     1.8 -  "char_case f c = (let n = nat_of_char c in f (nibble_of_nat (n div 16)) (nibble_of_nat n))"
     1.9 +lemma case_char_code [code]:
    1.10 +  "case_char f c = (let n = nat_of_char c in f (nibble_of_nat (n div 16)) (nibble_of_nat n))"
    1.11    by (cases c)
    1.12      (simp only: Let_def nibble_of_nat_of_char_div_16 nibble_of_nat_nat_of_char char.cases)
    1.13  
    1.14  lemma [code]:
    1.15 -  "char_rec = char_case"
    1.16 +  "rec_char = case_char"
    1.17    by (simp add: fun_eq_iff split: char.split)
    1.18  
    1.19  definition char_of_nat :: "nat \<Rightarrow> char" where