--- 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 ..
--- 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 ..