src/HOL/String.thy
changeset 39198 f967a16dfcdd
parent 38858 1920158cfa17
child 39250 548a3e5521ab
     1.1 --- a/src/HOL/String.thy	Mon Sep 06 22:58:06 2010 +0200
     1.2 +++ b/src/HOL/String.thy	Tue Sep 07 10:05:19 2010 +0200
     1.3 @@ -60,12 +60,12 @@
     1.4  
     1.5  lemma char_case_nibble_pair [code, code_unfold]:
     1.6    "char_case f = split f o nibble_pair_of_char"
     1.7 -  by (simp add: expand_fun_eq split: char.split)
     1.8 +  by (simp add: ext_iff split: char.split)
     1.9  
    1.10  lemma char_rec_nibble_pair [code, code_unfold]:
    1.11    "char_rec f = split f o nibble_pair_of_char"
    1.12    unfolding char_case_nibble_pair [symmetric]
    1.13 -  by (simp add: expand_fun_eq split: char.split)
    1.14 +  by (simp add: ext_iff split: char.split)
    1.15  
    1.16  syntax
    1.17    "_Char" :: "xstr => char"    ("CHR _")