src/HOL/Library/Code_Real_Approx_By_Float.thy
changeset 45496 5c0444d2abfe
parent 45494 e828ccc5c110
child 46530 d5d14046686f
--- 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