src/HOL/Word/Word.thy

--- a/src/HOL/Word/Word.thy	Thu Jul 01 08:13:20 2010 +0200
+++ b/src/HOL/Word/Word.thy	Thu Jul 01 13:32:14 2010 +0200
@@ -240,6 +240,10 @@
 
 end
 
+lemma [code]:
+  "msb a \<longleftrightarrow> bin_sign (sint a) = (- 1 :: int)"
+  by (simp only: word_msb_def Min_def)
+
 definition setBit :: "'a :: len0 word => nat => 'a word" where 
   "setBit w n == set_bit w n True"