# HG changeset patch
# User haftmann
# Date 1501757403 -7200
# Node ID f773691617c0be725cbf6ec8a07647affcca4841
# Parent  dcb3e6bdc00a4fdea1063116df73546a98bfc6a5
lifting setup for char

diff -r dcb3e6bdc00a -r f773691617c0 src/HOL/String.thy
--- 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>