src/HOL/Quickcheck.thy
changeset 31267 4a85a4afc97d
parent 31260 4d273d043d59
child 31483 88210717bfc8
     1.1 --- a/src/HOL/Quickcheck.thy	Wed May 27 22:11:05 2009 +0200
     1.2 +++ b/src/HOL/Quickcheck.thy	Wed May 27 22:11:05 2009 +0200
     1.3 @@ -73,6 +73,10 @@
     1.4  definition beyond :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral" where
     1.5    "beyond k l = (if l > k then l else 0)"
     1.6  
     1.7 +lemma beyond_zero:
     1.8 +  "beyond k 0 = 0"
     1.9 +  by (simp add: beyond_def)
    1.10 +
    1.11  use "Tools/quickcheck_generators.ML"
    1.12  setup {* Quickcheck_Generators.setup *}
    1.13  
    1.14 @@ -100,6 +104,8 @@
    1.15  end
    1.16  
    1.17  
    1.18 +hide (open) const collapse beyond
    1.19 +
    1.20  no_notation fcomp (infixl "o>" 60)
    1.21  no_notation scomp (infixl "o\<rightarrow>" 60)
    1.22