src/HOL/String.thy
changeset 64994 6e4c05e8edbb
parent 64630 96015aecfeba
child 66190 a41435469559
     1.1 --- a/src/HOL/String.thy	Mon Feb 06 20:56:37 2017 +0100
     1.2 +++ b/src/HOL/String.thy	Mon Feb 06 20:56:38 2017 +0100
     1.3 @@ -375,6 +375,17 @@
     1.4  lifting_update literal.lifting
     1.5  lifting_forget literal.lifting
     1.6  
     1.7 +  
     1.8 +subsection \<open>Dedicated conversion for generated computations\<close>
     1.9 +
    1.10 +definition char_of_num :: "num \<Rightarrow> char"
    1.11 +  where "char_of_num = char_of_nat o nat_of_num"
    1.12 +
    1.13 +lemma [code_computation_unfold]:
    1.14 +  "Char = char_of_num"
    1.15 +  by (simp add: fun_eq_iff char_of_num_def nat_of_num_numeral Char_def)
    1.16 +
    1.17 +
    1.18  subsection \<open>Code generator\<close>
    1.19  
    1.20  ML_file "Tools/string_code.ML"