src/HOL/Quickcheck_Exhaustive.thy
changeset 45818 53a697f5454a
parent 45750 17100f4ce0b5
child 45925 cd4243c025bb
     1.1 --- a/src/HOL/Quickcheck_Exhaustive.thy	Mon Dec 12 12:03:34 2011 +0100
     1.2 +++ b/src/HOL/Quickcheck_Exhaustive.thy	Mon Dec 12 13:45:54 2011 +0100
     1.3 @@ -430,8 +430,8 @@
     1.4  class fast_exhaustive = term_of +
     1.5    fixes fast_exhaustive :: "('a \<Rightarrow> unit) \<Rightarrow> code_numeral \<Rightarrow> unit"
     1.6  
     1.7 -consts throw_Counterexample :: "term list => unit"
     1.8 -consts catch_Counterexample :: "unit => term list option"
     1.9 +axiomatization throw_Counterexample :: "term list => unit"
    1.10 +axiomatization catch_Counterexample :: "unit => term list option"
    1.11  
    1.12  code_const throw_Counterexample
    1.13    (Quickcheck "raise (Exhaustive'_Generators.Counterexample _)")
    1.14 @@ -535,7 +535,16 @@
    1.15  
    1.16  hide_fact orelse_def
    1.17  no_notation orelse (infixr "orelse" 55)
    1.18 -hide_const (open) orelse unknown mk_map_term check_all_n_lists 
    1.19 +
    1.20 +hide_fact
    1.21 +  exhaustive'_def
    1.22 +  exhaustive_code_numeral'_def
    1.23 +
    1.24 +hide_const (open)
    1.25 +  exhaustive full_exhaustive exhaustive' exhaustive_code_numeral' full_exhaustive_code_numeral'
    1.26 +  throw_Counterexample catch_Counterexample
    1.27 +  check_all enum_term_of
    1.28 +  orelse unknown mk_map_term check_all_n_lists
    1.29  
    1.30  hide_type (open) cps pos_bound_cps neg_bound_cps unknown three_valued
    1.31  hide_const (open) cps_empty cps_single cps_bind cps_plus cps_if cps_not