src/HOL/Quickcheck_Exhaustive.thy
changeset 62364 9209770bdcdf
parent 61121 efe8b18306b7
child 62597 b3f2b8c906a6
     1.1 --- a/src/HOL/Quickcheck_Exhaustive.thy	Fri Feb 19 15:01:38 2016 +0100
     1.2 +++ b/src/HOL/Quickcheck_Exhaustive.thy	Thu Feb 18 17:52:52 2016 +0100
     1.3 @@ -630,8 +630,12 @@
     1.4         (Code_Evaluation.term_of (\<lambda>x y. char_of_nat (nat_of_nibble x * 16 + nat_of_nibble y))) (t1 ())) (t2 ()))))"
     1.5    by (simp add: check_all_char_def)
     1.6  
     1.7 -lemma full_exhaustive_char_code [code]:
     1.8 -  "full_exhaustive_class.full_exhaustive f i =
     1.9 +instantiation char :: full_exhaustive
    1.10 +begin
    1.11 +
    1.12 +definition full_exhaustive_char
    1.13 +where
    1.14 +  "full_exhaustive f i =
    1.15       (if 0 < i then full_exhaustive_class.full_exhaustive
    1.16         (\<lambda>(a, b). full_exhaustive_class.full_exhaustive
    1.17            (\<lambda>(c, d).
    1.18 @@ -641,7 +645,10 @@
    1.19                     (TYPEREP(nibble \<Rightarrow> nibble \<Rightarrow> char)))
    1.20                        (b ())) (d ()))) (i - 1)) (i - 1)
    1.21      else None)"
    1.22 -  by (simp add: typerep_fun_def typerep_char_def typerep_nibble_def String.char.full_exhaustive_char.simps)
    1.23 +
    1.24 +instance ..
    1.25 +
    1.26 +end
    1.27  
    1.28  hide_fact (open) orelse_def
    1.29  no_notation orelse (infixr "orelse" 55)