# HG changeset patch
# User kleing
# Date 1316139015 -36000
# Node ID 98e05fc1ce7dacea7b3228537557b11ab25f2454
# Parent  22c0857b8aab48518427dd8314192efa5a21002f
removed word_neq_0_conv from simpset, it's almost never wanted.

diff -r 22c0857b8aab -r 98e05fc1ce7d src/HOL/Word/Word.thy
--- 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 -