hiding randompred definitions
authorbulwahn
Tue, 27 Oct 2009 09:03:56 +0100
changeset 33254 d0c00b81db1d
parent 33253 d9ca0c3bf680
child 33255 75b01355e5d4
hiding randompred definitions
src/HOL/Quickcheck.thy
--- a/src/HOL/Quickcheck.thy	Tue Oct 27 09:03:56 2009 +0100
+++ b/src/HOL/Quickcheck.thy	Tue Oct 27 09:03:56 2009 +0100
@@ -177,7 +177,7 @@
 
 code_reserved Quickcheck Quickcheck_Generators
 
-
+hide (open) fact empty_def single_def bind_def union_def if_randompred_def not_randompred_def Random_def map_def
 hide (open) type randompred
 hide (open) const random collapse beyond random_fun_aux random_fun_lift
   empty single bind union if_randompred not_randompred Random map