# HG changeset patch
# User berghofe
# Date 1197912230 -3600
# Node ID 35a6c1b1c8e337f180c61873ab7c2b1c78f90c25
# Parent  5850301e83c7f8077ac028618def60f7bc125721
Added code lemma for message_string_size.

diff -r 5850301e83c7 -r 35a6c1b1c8e3 src/HOL/Library/Code_Message.thy
--- a/src/HOL/Library/Code_Message.thy	Mon Dec 17 18:22:48 2007 +0100
+++ b/src/HOL/Library/Code_Message.thy	Mon Dec 17 18:23:50 2007 +0100
@@ -17,6 +17,9 @@
 lemma [code func]: "size (s\<Colon>message_string) = 0"
   by (cases s) simp_all
 
+lemma [code func]: "message_string_size (s\<Colon>message_string) = 0"
+  by (cases s) simp_all
+
 subsection {* ML interface *}
 
 ML {*