# HG changeset patch
# User haftmann
# Date 1200901417 -3600
# Node ID 6e5b0f176dac0f672b391d8d396390c5018da7e2
# Parent  f43bac9def6ecb8e2918ad3c14de109692ed9a73
tuned proof

diff -r f43bac9def6e -r 6e5b0f176dac src/HOL/Word/Num_Lemmas.thy
--- a/src/HOL/Word/Num_Lemmas.thy	Mon Jan 21 08:43:36 2008 +0100
+++ b/src/HOL/Word/Num_Lemmas.thy	Mon Jan 21 08:43:37 2008 +0100
@@ -61,8 +61,8 @@
 lemmas PlsMin_simps [simp] = PlsMin_defs [THEN Eq_TrueI]
 
 lemma number_of_False_cong: 
-  "False ==> number_of x = number_of y" 
-  by auto
+  "False \<Longrightarrow> number_of x = number_of y"
+  by (rule FalseE)
 
 lemmas nat_simps = diff_add_inverse2 diff_add_inverse
 lemmas nat_iffs = le_add1 le_add2