--- a/src/HOL/Library/Code_Real_Approx_By_Float.thy Sat Feb 18 23:43:21 2012 +0100
+++ b/src/HOL/Library/Code_Real_Approx_By_Float.thy Sun Feb 12 22:10:33 2012 +0100
@@ -133,11 +133,11 @@
declare number_of_real_code [code_unfold del]
-lemma "False"
-proof-
- have "cos(pi/2) = 0" by(rule cos_pi_half)
- moreover have "cos(pi/2) \<noteq> 0" by eval
- ultimately show "False" by blast
-qed
+notepad
+begin
+ have "cos (pi/2) = 0" by (rule cos_pi_half)
+ moreover have "cos (pi/2) \<noteq> 0" by eval
+ ultimately have "False" by blast
+end
end