src/HOL/Word/WordArith.thy
changeset 25112 98824cc791c0
parent 24465 70f0214b3ecc
child 25134 3d4953e88449
     1.1 --- a/src/HOL/Word/WordArith.thy	Sat Oct 20 12:09:30 2007 +0200
     1.2 +++ b/src/HOL/Word/WordArith.thy	Sat Oct 20 12:09:33 2007 +0200
     1.3 @@ -117,7 +117,7 @@
     1.4  lemmas unat_eq_zero = unat_0_iff
     1.5  
     1.6  lemma unat_gt_0: "(0 < unat x) = (x ~= 0)"
     1.7 -  by (simp add : unat_0_iff [symmetric])
     1.8 +  by (simp add : neq0_conv unat_0_iff [symmetric])
     1.9  
    1.10  lemma ucast_0 [simp] : "ucast 0 = 0"
    1.11    unfolding ucast_def
    1.12 @@ -1245,7 +1245,7 @@
    1.13    apply (rule contrapos_np)
    1.14     prefer 2
    1.15     apply (erule card_infinite)
    1.16 -  apply (simp add : card_word)
    1.17 +  apply (simp add : card_word neq0_conv)
    1.18    done
    1.19  
    1.20  lemma card_word_size: