Mercurial Mercurial > repos > isabelle / 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 45952 ed9cc0634aaf
parent 45856 caa99836aed8
child 45953 1d6fcb19aa50 
--- a/src/HOL/Word/Bit_Representation.thy	Wed Dec 21 18:23:08 2011 +0100
+++ b/src/HOL/Word/Bit_Representation.thy	Thu Dec 22 12:14:26 2011 +0100
@@ -275,6 +275,9 @@
 lemma bin_nth_Pls [simp]: "~ bin_nth Int.Pls n"
   by (induct n) auto
 
+lemma bin_nth_minus1 [simp]: "bin_nth -1 n"
+  by (induct n) auto
+
 lemma bin_nth_Min [simp]: "bin_nth Int.Min n"
   by (induct n) auto
isabelle