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