Mercurial Mercurial > repos > testboard / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Word/Bit_Representation.thy
changeset 45953 1d6fcb19aa50
parent 45952 ed9cc0634aaf
child 45954 f67d3bb5f09c 
--- 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
testboard