Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
explicit size of characters
authorhaftmann
Tue, 16 Sep 2008 09:21:27 +0200
changeset 28230 87feb146d3d1
parent 28229 4f06fae6a55e
child 28231 7dd07bd7bebd
explicit size of characters
src/HOL/List.thy file | annotate | diff | comparison | revisions 
--- 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
isabelle