enforce quick_and_dirty in Code_Real_Approx_By_Float
authorhoelzl
Mon Nov 14 12:28:34 2011 +0100 (2011-11-14)
changeset 45494e828ccc5c110
parent 45490 20c8c0cca555
child 45495 c55a07526dbe
enforce quick_and_dirty in Code_Real_Approx_By_Float
src/HOL/Library/Code_Real_Approx_By_Float.thy
     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