src/HOL/Library/Code_Real_Approx_By_Float.thy
changeset 45494 e828ccc5c110
parent 45483 34d07cf7d207
child 45496 5c0444d2abfe
     1.1 --- a/src/HOL/Library/Code_Real_Approx_By_Float.thy	Mon Nov 14 17:48:26 2011 +0100
     1.2 +++ b/src/HOL/Library/Code_Real_Approx_By_Float.thy	Mon Nov 14 12:28:34 2011 +0100
     1.3 @@ -140,9 +140,7 @@
     1.4    ultimately show "False" by blast
     1.5  qed
     1.6  
     1.7 -definition "test = exp (sin 3) / 5 * cos 6 + arctan (arccos (arcsin 8))"
     1.8 -
     1.9 -export_code test
    1.10 -  in OCaml file -
    1.11 +lemma False
    1.12 +  sorry -- "Use quick_and_dirty to load this theory."
    1.13  
    1.14  end