added lemma beyond_zero; hide constants

--- a/src/HOL/Quickcheck.thy	Wed May 27 22:11:05 2009 +0200
+++ b/src/HOL/Quickcheck.thy	Wed May 27 22:11:05 2009 +0200
@@ -73,6 +73,10 @@
 definition beyond :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral" where
   "beyond k l = (if l > k then l else 0)"
 
+lemma beyond_zero:
+  "beyond k 0 = 0"
+  by (simp add: beyond_def)
+
 use "Tools/quickcheck_generators.ML"
 setup {* Quickcheck_Generators.setup *}
 
@@ -100,6 +104,8 @@
 end
 
 
+hide (open) const collapse beyond
+
 no_notation fcomp (infixl "o>" 60)
 no_notation scomp (infixl "o\<rightarrow>" 60)