src/HOL/Library/Code_Char_chr.thy
changeset 31998 2c7a24f74db9
parent 30663 0b6aff7451b2
child 32069 6d28bbd33e2c
     1.1 --- a/src/HOL/Library/Code_Char_chr.thy	Tue Jul 14 10:53:44 2009 +0200
     1.2 +++ b/src/HOL/Library/Code_Char_chr.thy	Tue Jul 14 10:54:04 2009 +0200
     1.3 @@ -24,11 +24,11 @@
     1.4  
     1.5  lemmas [code del] = char.recs char.cases char.size
     1.6  
     1.7 -lemma [code, code inline]:
     1.8 +lemma [code, code_inline]:
     1.9    "char_rec f c = split f (nibble_pair_of_nat (nat_of_char c))"
    1.10    by (cases c) (auto simp add: nibble_pair_of_nat_char)
    1.11  
    1.12 -lemma [code, code inline]:
    1.13 +lemma [code, code_inline]:
    1.14    "char_case f c = split f (nibble_pair_of_nat (nat_of_char c))"
    1.15    by (cases c) (auto simp add: nibble_pair_of_nat_char)
    1.16