src/HOL/String.thy
changeset 55642 63beb38e9258
parent 55428 0ab52bf7b5e6
child 55969 8820ddb8f9f4
     1.1 --- a/src/HOL/String.thy	Fri Feb 21 00:09:55 2014 +0100
     1.2 +++ b/src/HOL/String.thy	Fri Feb 21 00:09:56 2014 +0100
     1.3 @@ -289,7 +289,7 @@
     1.4  lemma case_char_code [code]:
     1.5    "case_char f c = (let n = nat_of_char c in f (nibble_of_nat (n div 16)) (nibble_of_nat n))"
     1.6    by (cases c)
     1.7 -    (simp only: Let_def nibble_of_nat_of_char_div_16 nibble_of_nat_nat_of_char char.cases)
     1.8 +    (simp only: Let_def nibble_of_nat_of_char_div_16 nibble_of_nat_nat_of_char char.case)
     1.9  
    1.10  lemma [code]:
    1.11    "rec_char = case_char"