# HG changeset patch
# User bulwahn
# Date 1323693954 -3600
# Node ID 53a697f5454ab3f08e613b6b4b4305cf8de84a9e
# Parent  bb39fba83e9b331c64b4e6fa3518649eeb031a1c
hiding constants and facts in the Quickcheck_Exhaustive and Quickcheck_Narrowing theory;

diff -r bb39fba83e9b -r 53a697f5454a src/HOL/Quickcheck_Exhaustive.thy
--- 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
diff -r bb39fba83e9b -r 53a697f5454a src/HOL/Quickcheck_Narrowing.thy
--- a/src/HOL/Quickcheck_Narrowing.thy	Mon Dec 12 12:03:34 2011 +0100
+++ b/src/HOL/Quickcheck_Narrowing.thy	Mon Dec 12 13:45:54 2011 +0100
@@ -448,7 +448,7 @@
 *)
 
 hide_type code_int narrowing_type narrowing_term cons property
-hide_const int_of of_int nth error toEnum marker empty C conv nonEmpty ensure_testable all exists 
+hide_const int_of of_int nat_of map_cons nth error toEnum marker empty C conv nonEmpty ensure_testable all exists drawn_from around_zero
 hide_const (open) Var Ctr "apply" sum cons
 hide_fact empty_def cons_def conv.simps nonEmpty.simps apply_def sum_def ensure_testable_def all_def exists_def
 
diff -r bb39fba83e9b -r 53a697f5454a src/HOL/Rat.thy
--- a/src/HOL/Rat.thy	Mon Dec 12 12:03:34 2011 +0100
+++ b/src/HOL/Rat.thy	Mon Dec 12 13:45:54 2011 +0100
@@ -1158,7 +1158,7 @@
 begin
 
 definition
-  "exhaustive f d = exhaustive (%l. exhaustive (%k. f (Fract k (Code_Numeral.int_of l + 1))) d) d"
+  "exhaustive_rat f d = Quickcheck_Exhaustive.exhaustive (%l. Quickcheck_Exhaustive.exhaustive (%k. f (Fract k (Code_Numeral.int_of l + 1))) d) d"
 
 instance ..
 
@@ -1168,7 +1168,7 @@
 begin
 
 definition
-  "full_exhaustive f d = full_exhaustive (%(l, _). full_exhaustive (%k.
+  "full_exhaustive_rat f d = Quickcheck_Exhaustive.full_exhaustive (%(l, _). Quickcheck_Exhaustive.full_exhaustive (%k.
      f (let j = Code_Numeral.int_of l + 1
         in valterm_fract k (j, %_. Code_Evaluation.term_of j))) d) d"
 
diff -r bb39fba83e9b -r 53a697f5454a src/HOL/RealDef.thy
--- a/src/HOL/RealDef.thy	Mon Dec 12 12:03:34 2011 +0100
+++ b/src/HOL/RealDef.thy	Mon Dec 12 13:45:54 2011 +0100
@@ -1729,7 +1729,7 @@
 begin
 
 definition
-  "exhaustive f d = exhaustive (%r. f (Ratreal r)) d"
+  "exhaustive_real f d = Quickcheck_Exhaustive.exhaustive (%r. f (Ratreal r)) d"
 
 instance ..
 
@@ -1739,7 +1739,7 @@
 begin
 
 definition
-  "full_exhaustive f d = full_exhaustive (%r. f (valterm_ratreal r)) d"
+  "full_exhaustive_real f d = Quickcheck_Exhaustive.full_exhaustive (%r. f (valterm_ratreal r)) d"
 
 instance ..