# HG changeset patch
# User huffman
# Date 1334856750 -7200
# Node ID e3c699a1fae6697dd8c8f2d2c1fded41ddc43ec0
# Parent  261f9de35b181f28be0ac3f3662bcdeae82d43a3
add code lemmas for word operations

diff -r 261f9de35b18 -r e3c699a1fae6 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Thu Apr 19 19:18:47 2012 +0200
+++ b/src/HOL/Word/Word.thy	Thu Apr 19 19:32:30 2012 +0200
@@ -294,7 +294,7 @@
 
 text {* Legacy theorems: *}
 
-lemma word_arith_wis: shows
+lemma word_arith_wis [code]: shows
   word_add_def: "a + b = word_of_int (uint a + uint b)" and
   word_sub_wi: "a - b = word_of_int (uint a - uint b)" and
   word_mult_def: "a * b = word_of_int (uint a * uint b)" and
@@ -416,7 +416,7 @@
 
 end
 
-lemma shows
+lemma [code]: shows
   word_not_def: "NOT (a::'a::len0 word) = word_of_int (NOT (uint a))" and
   word_and_def: "(a::'a word) AND b = word_of_int (uint a AND uint b)" and
   word_or_def: "(a::'a word) OR b = word_of_int (uint a OR uint b)" and