src/HOL/Library/Code_Char.thy

--- a/src/HOL/Library/Code_Char.thy	Fri Jan 25 14:53:58 2008 +0100
+++ b/src/HOL/Library/Code_Char.thy	Fri Jan 25 14:54:41 2008 +0100
@@ -9,6 +9,16 @@
 imports List
 begin
 
+declare char.recs [code func del] char.cases [code func del]
+
+lemma [code func]:
+  "size (c\<Colon>char) = 0"
+  by (cases c) simp
+
+lemma [code func]:
+  "char_size (c\<Colon>char) = 0"
+  by (cases c) simp
+
 code_type char
   (SML "char")
   (OCaml "char")