# HG changeset patch
# User haftmann
# Date 1329081033 -3600
# Node ID d5d14046686f2c07f2d2fc76dfe4d86e9db64393
# Parent  a018d542e0ae5f82a226c5e6626a2b1f984b36e6
notepad is more appropriate here

diff -r a018d542e0ae -r d5d14046686f src/HOL/Library/Code_Real_Approx_By_Float.thy
--- 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