author | berghofe |
Mon, 17 Dec 2007 18:23:50 +0100 | |
changeset 25673 | 35a6c1b1c8e3 |
parent 25672 | 5850301e83c7 |
child 25674 | b04508c59b9d |
--- 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 {*