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.
removed word_neq_0_conv from simpset, it's almost never wanted.
authorkleing
Fri, 16 Sep 2011 12:10:15 +1000
changeset 44938 98e05fc1ce7d
parent 44937 22c0857b8aab
child 44939 5930d35c976d
removed word_neq_0_conv from simpset, it's almost never wanted.
src/HOL/Word/Word.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Word/Word.thy	Thu Sep 15 12:40:08 2011 -0400
+++ b/src/HOL/Word/Word.thy	Fri Sep 16 12:10:15 2011 +1000
@@ -4514,7 +4514,7 @@
   apply (simp add:  mod_nat_add word_size)
   done
 
-lemma word_neq_0_conv [simp]:
+lemma word_neq_0_conv:
   fixes w :: "'a :: len word"
   shows "(w \<noteq> 0) = (0 < w)"
 proof -
isabelle