Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/ex/Hilbert_Classical.thy
changeset 11635 fd242f857508
parent 11591 4b171ad4ff65
child 14981 e73f8140af78 
--- a/src/HOL/ex/Hilbert_Classical.thy	Fri Sep 28 19:24:25 2001 +0200
+++ b/src/HOL/ex/Hilbert_Classical.thy	Fri Sep 28 20:08:05 2001 +0200
@@ -52,8 +52,7 @@
 	hence "Eps ?P = Eps ?Q" by (rule arg_cong)
 	also note P
 	also note Q
-	finally have "False = True" .	
-	thus False by (rule False_neq_True)
+	finally show False by (rule False_neq_True)
       qed
       have "\<not> A"
       proof
isabelle