# HG changeset patch
# User haftmann
# Date 1221549687 -7200
# Node ID 87feb146d3d118256b84e01a805f1009dc064420
# Parent  4f06fae6a55e59f41fd48548cbc911f05c29d25b
explicit size of characters

diff -r 4f06fae6a55e -r 87feb146d3d1 src/HOL/List.thy
--- a/src/HOL/List.thy	Tue Sep 16 09:21:26 2008 +0200
+++ b/src/HOL/List.thy	Tue Sep 16 09:21:27 2008 +0200
@@ -3370,6 +3370,12 @@
 instance char :: finite
   by default (simp add: UNIV_char)
 
+lemma size_char [code, simp]:
+  "size (c::char) = 0" by (cases c) simp
+
+lemma char_size [code, simp]:
+  "char_size (c::char) = 0" by (cases c) simp
+
 types string = "char list"
 
 syntax