src/HOL/String.thy
changeset 61032 b57df8eecad6
parent 60801 7664e0916eec
child 61076 bdc1e2f0a86a
     1.1 --- a/src/HOL/String.thy	Thu Aug 27 13:07:45 2015 +0200
     1.2 +++ b/src/HOL/String.thy	Thu Aug 27 21:19:48 2015 +0200
     1.3 @@ -128,9 +128,9 @@
     1.4  ML_file "Tools/string_syntax.ML"
     1.5  
     1.6  lemma UNIV_char:
     1.7 -  "UNIV = image (split Char) (UNIV \<times> UNIV)"
     1.8 +  "UNIV = image (case_prod Char) (UNIV \<times> UNIV)"
     1.9  proof (rule UNIV_eq_I)
    1.10 -  fix x show "x \<in> image (split Char) (UNIV \<times> UNIV)" by (cases x) auto
    1.11 +  fix x show "x \<in> image (case_prod Char) (UNIV \<times> UNIV)" by (cases x) auto
    1.12  qed
    1.13  
    1.14  lemma size_char [code, simp]:
    1.15 @@ -218,7 +218,7 @@
    1.16    "Enum.enum_ex P \<longleftrightarrow> list_ex P (Enum.enum :: char list)"
    1.17  
    1.18  lemma enum_char_product_enum_nibble:
    1.19 -  "(Enum.enum :: char list) = map (split Char) (List.product Enum.enum Enum.enum)"
    1.20 +  "(Enum.enum :: char list) = map (case_prod Char) (List.product Enum.enum Enum.enum)"
    1.21    by (simp add: enum_char_def enum_nibble_def)
    1.22  
    1.23  instance proof