Added code lemma for message_string_size.
authorberghofe
Mon, 17 Dec 2007 18:23:50 +0100
changeset 25673 35a6c1b1c8e3
parent 25672 5850301e83c7
child 25674 b04508c59b9d
Added code lemma for message_string_size.
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 {*