src/HOL/Quickcheck_Exhaustive.thy
changeset 45750 17100f4ce0b5
parent 45733 6bb30ae1abfe
child 45818 53a697f5454a
     1.1 --- a/src/HOL/Quickcheck_Exhaustive.thy	Sun Dec 04 18:30:57 2011 +0100
     1.2 +++ b/src/HOL/Quickcheck_Exhaustive.thy	Sun Dec 04 20:05:08 2011 +0100
     1.3 @@ -466,7 +466,7 @@
     1.4  where
     1.5    "cps_not n = (%c. case n (%u. Some []) of None => c () | Some _ => None)"
     1.6  
     1.7 -type_synonym 'a pos_bound_cps = "('a => term list option) => code_numeral => term list option"
     1.8 +type_synonym 'a pos_bound_cps = "('a => (bool * term list) option) => code_numeral => (bool * term list) option"
     1.9  
    1.10  definition pos_bound_cps_empty :: "'a pos_bound_cps"
    1.11  where
    1.12 @@ -515,7 +515,7 @@
    1.13  
    1.14  definition neg_bound_cps_not :: "unit pos_bound_cps => unit neg_bound_cps"
    1.15  where
    1.16 -  "neg_bound_cps_not n = (%c i. case n (%u. Some []) i of None => c (Known ()) | Some _ => No_value)"
    1.17 +  "neg_bound_cps_not n = (%c i. case n (%u. Some (True, [])) i of None => c (Known ()) | Some _ => No_value)"
    1.18  
    1.19  definition pos_bound_cps_not :: "unit neg_bound_cps => unit pos_bound_cps"
    1.20  where