tuned proof
authorhaftmann
Mon Jan 21 08:43:37 2008 +0100 (2008-01-21)
changeset 259376e5b0f176dac
parent 25936 f43bac9def6e
child 25938 2c1c0e989615
tuned proof
src/HOL/Word/Num_Lemmas.thy
     1.1 --- a/src/HOL/Word/Num_Lemmas.thy	Mon Jan 21 08:43:36 2008 +0100
     1.2 +++ b/src/HOL/Word/Num_Lemmas.thy	Mon Jan 21 08:43:37 2008 +0100
     1.3 @@ -61,8 +61,8 @@
     1.4  lemmas PlsMin_simps [simp] = PlsMin_defs [THEN Eq_TrueI]
     1.5  
     1.6  lemma number_of_False_cong: 
     1.7 -  "False ==> number_of x = number_of y" 
     1.8 -  by auto
     1.9 +  "False \<Longrightarrow> number_of x = number_of y"
    1.10 +  by (rule FalseE)
    1.11  
    1.12  lemmas nat_simps = diff_add_inverse2 diff_add_inverse
    1.13  lemmas nat_iffs = le_add1 le_add2