--- a/src/HOL/Word/Bits_Int.thy Sat Dec 28 21:06:25 2013 +0100
+++ b/src/HOL/Word/Bits_Int.thy Sat Dec 28 21:06:26 2013 +0100
@@ -384,14 +384,14 @@
subsection {* Setting and clearing bits *}
+(** nth bit, set/clear **)
+
primrec
bin_sc :: "nat => bool => int => int"
where
Z: "bin_sc 0 b w = bin_rest w BIT b"
| Suc: "bin_sc (Suc n) b w = bin_sc n b (bin_rest w) BIT bin_last w"
-(** nth bit, set/clear **)
-
lemma bin_nth_sc [simp]:
"bin_nth (bin_sc n b w) n \<longleftrightarrow> b"
by (induct n arbitrary: w) auto