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.
tuned proof
authorhaftmann
Mon, 21 Jan 2008 08:43:37 +0100
changeset 25937 6e5b0f176dac
parent 25936 f43bac9def6e
child 25938 2c1c0e989615
tuned proof
src/HOL/Word/Num_Lemmas.thy file | annotate | diff | comparison | revisions 
--- 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
isabelle