src/HOL/String.thy
changeset 32069 6d28bbd33e2c
parent 31998 2c7a24f74db9
child 33063 4d462963a7db
     1.1 --- a/src/HOL/String.thy	Tue Jul 14 16:27:31 2009 +0200
     1.2 +++ b/src/HOL/String.thy	Tue Jul 14 16:27:32 2009 +0200
     1.3 @@ -58,11 +58,11 @@
     1.4  end
     1.5  *}
     1.6  
     1.7 -lemma char_case_nibble_pair [code, code_inline]:
     1.8 +lemma char_case_nibble_pair [code, code_unfold]:
     1.9    "char_case f = split f o nibble_pair_of_char"
    1.10    by (simp add: expand_fun_eq split: char.split)
    1.11  
    1.12 -lemma char_rec_nibble_pair [code, code_inline]:
    1.13 +lemma char_rec_nibble_pair [code, code_unfold]:
    1.14    "char_rec f = split f o nibble_pair_of_char"
    1.15    unfolding char_case_nibble_pair [symmetric]
    1.16    by (simp add: expand_fun_eq split: char.split)