# HG changeset patch
# User hoelzl
# Date 1321270114 -3600
# Node ID e828ccc5c110f68bab166eb6daf16566294398e7
# Parent  20c8c0cca555cc5f9d4e03ae07edde28448797c4
enforce quick_and_dirty in Code_Real_Approx_By_Float

diff -r 20c8c0cca555 -r e828ccc5c110 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