--- a/src/HOL/String.thy Thu Aug 03 12:50:02 2017 +0200
+++ b/src/HOL/String.thy Thu Aug 03 12:50:03 2017 +0200
@@ -16,6 +16,8 @@
show "Suc 0 \<in> {n. n < 256}" by simp
qed
+setup_lifting type_definition_char
+
definition char_of_nat :: "nat \<Rightarrow> char"
where
"char_of_nat n = Abs_char (n mod 256)"
@@ -304,6 +306,9 @@
"char_of_integer n = Enum.enum ! (nat_of_integer n mod 256)"
by (simp add: char_of_integer_def enum_char_unfold)
+lifting_update char.lifting
+lifting_forget char.lifting
+
subsection \<open>Strings as dedicated type\<close>