--- a/src/HOL/Word/Bit_Representation.thy Thu Dec 22 12:14:26 2011 +0100
+++ b/src/HOL/Word/Bit_Representation.thy Fri Dec 23 11:50:12 2011 +0100
@@ -91,9 +91,6 @@
"(v BIT b <= w BIT c) = (v < w | v <= w & (b ~= (1::bit) | c ~= (0::bit)))"
unfolding Bit_def by (auto simp add: bitval_def split: bit.split)
-lemma no_no [simp]: "number_of (number_of i) = i"
- unfolding number_of_eq by simp
-
lemma Bit_B0:
"k BIT (0::bit) = k + k"
by (unfold Bit_def) simp
--- a/src/HOL/Word/Word.thy Thu Dec 22 12:14:26 2011 +0100
+++ b/src/HOL/Word/Word.thy Fri Dec 23 11:50:12 2011 +0100
@@ -1325,9 +1325,6 @@
lemmas unat_mono = word_less_nat_alt [THEN iffD1]
-lemma no_no [simp] : "number_of (number_of b) = number_of b"
- by (simp add: number_of_eq)
-
lemma unat_minus_one: "x ~= 0 \<Longrightarrow> unat (x - 1) = unat x - 1"
apply (unfold unat_def)
apply (simp only: int_word_uint word_arith_alts rdmods)