1.1 --- a/src/HOL/Library/Code_Real_Approx_By_Float.thy	Sat Feb 18 23:43:21 2012 +0100
     1.2 +++ b/src/HOL/Library/Code_Real_Approx_By_Float.thy	Sun Feb 12 22:10:33 2012 +0100
     1.3 @@ -133,11 +133,11 @@
     1.4  
     1.5  declare number_of_real_code [code_unfold del]
     1.6  
     1.7 -lemma "False"
     1.8 -proof-
     1.9 -  have "cos(pi/2) = 0" by(rule cos_pi_half)
    1.10 -  moreover have "cos(pi/2) \<noteq> 0" by eval
    1.11 -  ultimately show "False" by blast
    1.12 -qed
    1.13 +notepad
    1.14 +begin
    1.15 +  have "cos (pi/2) = 0" by (rule cos_pi_half)
    1.16 +  moreover have "cos (pi/2) \<noteq> 0" by eval
    1.17 +  ultimately have "False" by blast
    1.18 +end
    1.19  
    1.20  end