# HG changeset patch
# User bulwahn
# Date 1302273074 -7200
# Node ID eb32a8474a57b72996a46eaddad50ddb07a95c1c
# Parent  c664cc5cc5e934a0e96cb646e676107c3e67c9c9
rational and real instances for new compilation scheme for exhaustive quickcheck

diff -r c664cc5cc5e9 -r eb32a8474a57 src/HOL/Rat.thy
--- a/src/HOL/Rat.thy	Fri Apr 08 16:31:14 2011 +0200
+++ b/src/HOL/Rat.thy	Fri Apr 08 16:31:14 2011 +0200
@@ -1136,7 +1136,17 @@
 begin
 
 definition
-  "exhaustive f d = exhaustive (%(k, kt). exhaustive (%(l, lt).
+  "exhaustive f d = exhaustive (%k. exhaustive (%l. f (Fract (Code_Numeral.int_of k) (Code_Numeral.int_of l))) d) d"
+
+instance ..
+
+end
+
+instantiation rat :: full_exhaustive
+begin
+
+definition
+  "full_exhaustive f d = full_exhaustive (%(k, kt). full_exhaustive (%(l, lt).
      f (valterm_fract (Code_Numeral.int_of k, %_. Code_Evaluation.term_of (Code_Numeral.int_of k)) (Code_Numeral.int_of l, %_. Code_Evaluation.term_of (Code_Numeral.int_of l)))) d) d"
 
 instance ..
diff -r c664cc5cc5e9 -r eb32a8474a57 src/HOL/RealDef.thy
--- a/src/HOL/RealDef.thy	Fri Apr 08 16:31:14 2011 +0200
+++ b/src/HOL/RealDef.thy	Fri Apr 08 16:31:14 2011 +0200
@@ -1772,7 +1772,17 @@
 begin
 
 definition
-  "exhaustive f d = exhaustive (%r. f (valterm_ratreal r)) d"
+  "exhaustive f d = exhaustive (%r. f (Ratreal r)) d"
+
+instance ..
+
+end
+
+instantiation real :: full_exhaustive
+begin
+
+definition
+  "full_exhaustive f d = full_exhaustive (%r. f (valterm_ratreal r)) d"
 
 instance ..