Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add lemma bin_nth_minus1
authorhuffman
Thu, 22 Dec 2011 12:14:26 +0100
changeset 45952 ed9cc0634aaf
parent 45951 e49e45fee615
child 45953 1d6fcb19aa50
add lemma bin_nth_minus1
src/HOL/Word/Bit_Representation.thy file | annotate | diff | comparison | revisions 
--- 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