# HG changeset patch
# User haftmann
# Date 1243455065 -7200
# Node ID 4a85a4afc97d4a6719b3c19f66a711f8992bc03a
# Parent  55e70b6d812ec7dafce7e6b92ebf6f36f171c27d
added lemma beyond_zero; hide constants

diff -r 55e70b6d812e -r 4a85a4afc97d src/HOL/Quickcheck.thy
--- 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)