# HG changeset patch
# User huffman
# Date 1324637412 -3600
# Node ID 1d6fcb19aa503d5a03e45ef7c190d674bd1ef32c
# Parent  ed9cc0634aafecf5c946cd78893aa907385bbb80
remove two conflicting simp rules for 'number_of (number_of _)' pattern

diff -r ed9cc0634aaf -r 1d6fcb19aa50 src/HOL/Word/Bit_Representation.thy
--- 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
diff -r ed9cc0634aaf -r 1d6fcb19aa50 src/HOL/Word/Word.thy
--- 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)