src/HOL/Library/DAList.thy
changeset 51143 0a2371e7ced3
parent 51126 df86080de4cb
child 55565 f663fc1e653b
     1.1 --- a/src/HOL/Library/DAList.thy	Fri Feb 15 08:31:30 2013 +0100
     1.2 +++ b/src/HOL/Library/DAList.thy	Fri Feb 15 08:31:31 2013 +0100
     1.3 @@ -136,7 +136,7 @@
     1.4  instantiation alist :: (exhaustive, exhaustive) exhaustive
     1.5  begin
     1.6  
     1.7 -fun exhaustive_alist :: "(('a, 'b) alist => (bool * term list) option) => code_numeral => (bool * term list) option"
     1.8 +fun exhaustive_alist :: "(('a, 'b) alist => (bool * term list) option) => natural => (bool * term list) option"
     1.9  where
    1.10    "exhaustive_alist f i = (if i = 0 then None else case f empty of Some ts => Some ts | None =>
    1.11       exhaustive_alist (%a. Quickcheck_Exhaustive.exhaustive (%k. Quickcheck_Exhaustive.exhaustive (%v. f (update k v a)) (i - 1)) (i - 1)) (i - 1))"
    1.12 @@ -148,7 +148,7 @@
    1.13  instantiation alist :: (full_exhaustive, full_exhaustive) full_exhaustive
    1.14  begin
    1.15  
    1.16 -fun full_exhaustive_alist :: "(('a, 'b) alist * (unit => term) => (bool * term list) option) => code_numeral => (bool * term list) option"
    1.17 +fun full_exhaustive_alist :: "(('a, 'b) alist * (unit => term) => (bool * term list) option) => natural => (bool * term list) option"
    1.18  where
    1.19    "full_exhaustive_alist f i = (if i = 0 then None else case f valterm_empty of Some ts => Some ts | None =>
    1.20       full_exhaustive_alist (%a. Quickcheck_Exhaustive.full_exhaustive (%k. Quickcheck_Exhaustive.full_exhaustive (%v. f (valterm_update k v a)) (i - 1)) (i - 1)) (i - 1))"