--- a/src/HOL/Decision_Procs/Approximation.thy Wed Nov 12 17:37:43 2014 +0100
+++ b/src/HOL/Decision_Procs/Approximation.thy Wed Nov 12 17:37:43 2014 +0100
@@ -3494,7 +3494,8 @@
| term_of_bool false = @{term False};
val mk_int = HOLogic.mk_number @{typ int} o @{code integer_of_int};
- val dest_int = @{code int_of_integer} o snd o HOLogic.dest_number;
+ fun dest_int (@{term int_of_integer} $ j) = @{code int_of_integer} (snd (HOLogic.dest_number j))
+ | dest_int i = @{code int_of_integer} (snd (HOLogic.dest_number i));
fun term_of_float (@{code Float} (k, l)) =
@{term Float} $ mk_int k $ mk_int l;
@@ -3706,4 +3707,11 @@
ML_file "approximation.ML"
+
+section "Quickcheck Generator"
+
+ML_file "approximation_generator.ML"
+
+setup "Approximation_Generator.setup"
+
end