src/HOL/Library/Code_Real_Approx_By_Float.thy

--- a/src/HOL/Library/Code_Real_Approx_By_Float.thy	Mon Nov 14 17:48:26 2011 +0100
+++ b/src/HOL/Library/Code_Real_Approx_By_Float.thy	Mon Nov 14 12:28:34 2011 +0100
@@ -140,9 +140,7 @@
   ultimately show "False" by blast
 qed
 
-definition "test = exp (sin 3) / 5 * cos 6 + arctan (arccos (arcsin 8))"
-
-export_code test
-  in OCaml file -
+lemma False
+  sorry -- "Use quick_and_dirty to load this theory."
 
 end