# HG changeset patch
# User hoelzl
# Date 1321301491 -3600
# Node ID 5c0444d2abfea88c81fd1ec2d5875754bf823ae6
# Parent  c55a07526dbee42c9b3d3f2b192349f64ec20e24
remove sorry, otherwise it breaks the testboard

diff -r c55a07526dbe -r 5c0444d2abfe src/HOL/Library/Code_Real_Approx_By_Float.thy
--- a/src/HOL/Library/Code_Real_Approx_By_Float.thy	Mon Nov 14 18:36:31 2011 +0100
+++ b/src/HOL/Library/Code_Real_Approx_By_Float.thy	Mon Nov 14 21:11:31 2011 +0100
@@ -140,7 +140,4 @@
   ultimately show "False" by blast
 qed
 
-lemma False
-  sorry -- "Use quick_and_dirty to load this theory."
-
 end