src/HOL/Rat.thy
changeset 42311 eb32a8474a57
parent 41920 d4fb7a418152
child 43732 6b2bdc57155b
     1.1 --- a/src/HOL/Rat.thy	Fri Apr 08 16:31:14 2011 +0200
     1.2 +++ b/src/HOL/Rat.thy	Fri Apr 08 16:31:14 2011 +0200
     1.3 @@ -1136,7 +1136,17 @@
     1.4  begin
     1.5  
     1.6  definition
     1.7 -  "exhaustive f d = exhaustive (%(k, kt). exhaustive (%(l, lt).
     1.8 +  "exhaustive f d = exhaustive (%k. exhaustive (%l. f (Fract (Code_Numeral.int_of k) (Code_Numeral.int_of l))) d) d"
     1.9 +
    1.10 +instance ..
    1.11 +
    1.12 +end
    1.13 +
    1.14 +instantiation rat :: full_exhaustive
    1.15 +begin
    1.16 +
    1.17 +definition
    1.18 +  "full_exhaustive f d = full_exhaustive (%(k, kt). full_exhaustive (%(l, lt).
    1.19       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"
    1.20  
    1.21  instance ..