src/HOL/Quickcheck_Examples/Hotel_Example.thy
changeset 51143 0a2371e7ced3
parent 48255 968602739b54
child 51272 9c8d63b4b6be
     1.1 --- a/src/HOL/Quickcheck_Examples/Hotel_Example.thy	Fri Feb 15 08:31:30 2013 +0100
     1.2 +++ b/src/HOL/Quickcheck_Examples/Hotel_Example.thy	Fri Feb 15 08:31:31 2013 +0100
     1.3 @@ -105,8 +105,8 @@
     1.4    [code]: "cps_of_set (set xs) f = find_first f xs"
     1.5  sorry
     1.6  
     1.7 -consts pos_cps_of_set :: "'a set => ('a => (bool * term list) option) => code_numeral => (bool * term list) option"
     1.8 -consts neg_cps_of_set :: "'a set => ('a Quickcheck_Exhaustive.unknown => term list Quickcheck_Exhaustive.three_valued) => code_numeral => term list Quickcheck_Exhaustive.three_valued"
     1.9 +consts pos_cps_of_set :: "'a set => ('a => (bool * term list) option) => natural => (bool * term list) option"
    1.10 +consts neg_cps_of_set :: "'a set => ('a Quickcheck_Exhaustive.unknown => term list Quickcheck_Exhaustive.three_valued) => natural => term list Quickcheck_Exhaustive.three_valued"
    1.11  
    1.12  lemma
    1.13    [code]: "pos_cps_of_set (set xs) f i = find_first f xs"