# HG changeset patch
# User bulwahn
# Date 1323443312 -3600
# Node ID 5616fbda86e6ed33d0b669816e24b0c386dc01c9
# Parent  e832acb88f43b33fe278322b90e6c9ad54fea7e4
hiding definitional facts in Quickcheck; introducing catch_match more honestly

diff -r e832acb88f43 -r 5616fbda86e6 src/HOL/Quickcheck.thy
--- a/src/HOL/Quickcheck.thy	Fri Dec 09 14:46:18 2011 +0100
+++ b/src/HOL/Quickcheck.thy	Fri Dec 09 16:08:32 2011 +0100
@@ -16,9 +16,7 @@
 
 subsection {* Catching Match exceptions *}
 
-definition catch_match :: "'a => 'a => 'a" (* "(bool * term list) option => (bool * term list) option => (bool * term list) option"*)
-where
-  [code del]: "catch_match t1 t2 = (SOME t. t = t1 \<or> t = t2)"
+axiomatization catch_match :: "'a => 'a => 'a"
 
 code_const catch_match 
   (Quickcheck "(_) handle Match => _")
@@ -157,9 +155,6 @@
 no_notation fcomp (infixl "\<circ>>" 60)
 no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
 
-hide_fact catch_match_def
-hide_const (open) catch_match
-
 subsection {* The Random-Predicate Monad *} 
 
 fun iter' ::
@@ -220,9 +215,23 @@
 definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a randompred \<Rightarrow> 'b randompred)"
   where "map f P = bind P (single o f)"
 
-hide_fact (open) iter'.simps iter_def empty_def single_def bind_def union_def if_randompred_def iterate_upto_def not_randompred_def Random_def map_def
+hide_fact
+  random_bool_def random_bool_def_raw
+  random_itself_def random_itself_def_raw
+  random_char_def random_char_def_raw
+  random_literal_def random_literal_def_raw
+  random_nat_def random_nat_def_raw
+  random_int_def random_int_def_raw
+  random_fun_lift_def random_fun_lift_def_raw
+  random_fun_def random_fun_def_raw
+  collapse_def collapse_def_raw
+  beyond_def beyond_def_raw beyond_zero
+  random_aux_rec
+
+hide_const (open) catch_match random collapse beyond random_fun_aux random_fun_lift
+
+hide_fact (open) iter'.simps iter_def empty_def single_def bind_def union_def if_randompred_def iterate_upto_def not_randompred_def Random_def map_def 
 hide_type (open) randompred
-hide_const (open) random collapse beyond random_fun_aux random_fun_lift
-  iter' iter empty single bind union if_randompred iterate_upto not_randompred Random map
+hide_const (open) iter' iter empty single bind union if_randompred iterate_upto not_randompred Random map
 
 end