src/HOL/Quickcheck_Exhaustive.thy
changeset 45818 53a697f5454a
parent 45750 17100f4ce0b5
child 45925 cd4243c025bb
--- a/src/HOL/Quickcheck_Exhaustive.thy	Mon Dec 12 12:03:34 2011 +0100
+++ b/src/HOL/Quickcheck_Exhaustive.thy	Mon Dec 12 13:45:54 2011 +0100
@@ -430,8 +430,8 @@
 class fast_exhaustive = term_of +
   fixes fast_exhaustive :: "('a \<Rightarrow> unit) \<Rightarrow> code_numeral \<Rightarrow> unit"
 
-consts throw_Counterexample :: "term list => unit"
-consts catch_Counterexample :: "unit => term list option"
+axiomatization throw_Counterexample :: "term list => unit"
+axiomatization catch_Counterexample :: "unit => term list option"
 
 code_const throw_Counterexample
   (Quickcheck "raise (Exhaustive'_Generators.Counterexample _)")
@@ -535,7 +535,16 @@
 
 hide_fact orelse_def
 no_notation orelse (infixr "orelse" 55)
-hide_const (open) orelse unknown mk_map_term check_all_n_lists 
+
+hide_fact
+  exhaustive'_def
+  exhaustive_code_numeral'_def
+
+hide_const (open)
+  exhaustive full_exhaustive exhaustive' exhaustive_code_numeral' full_exhaustive_code_numeral'
+  throw_Counterexample catch_Counterexample
+  check_all enum_term_of
+  orelse unknown mk_map_term check_all_n_lists
 
 hide_type (open) cps pos_bound_cps neg_bound_cps unknown three_valued
 hide_const (open) cps_empty cps_single cps_bind cps_plus cps_if cps_not