1.1 --- a/src/HOL/ex/Hilbert_Classical.thy	Fri Sep 28 19:24:25 2001 +0200
     1.2 +++ b/src/HOL/ex/Hilbert_Classical.thy	Fri Sep 28 20:08:05 2001 +0200
     1.3 @@ -52,8 +52,7 @@
     1.4  	hence "Eps ?P = Eps ?Q" by (rule arg_cong)
     1.5  	also note P
     1.6  	also note Q
     1.7 -	finally have "False = True" .	
     1.8 -	thus False by (rule False_neq_True)
     1.9 +	finally show False by (rule False_neq_True)
    1.10        qed
    1.11        have "\<not> A"
    1.12        proof