remove sorry, otherwise it breaks the testboard
authorhoelzl
Mon, 14 Nov 2011 21:11:31 +0100
changeset 45496 5c0444d2abfe
parent 45495 c55a07526dbe
child 45497 4a23d6cb6cda
remove sorry, otherwise it breaks the testboard
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