src/HOL/Quickcheck_Exhaustive.thy
changeset 42230 594480d25aaa
parent 42195 1e7b62c93f5d
child 42274 50850486f8dc
     1.1 --- a/src/HOL/Quickcheck_Exhaustive.thy	Tue Apr 05 08:53:52 2011 +0200
     1.2 +++ b/src/HOL/Quickcheck_Exhaustive.thy	Tue Apr 05 09:38:23 2011 +0200
     1.3 @@ -360,18 +360,6 @@
     1.4  class bounded_forall =
     1.5    fixes bounded_forall :: "('a \<Rightarrow> bool) \<Rightarrow> code_numeral \<Rightarrow> bool"
     1.6  
     1.7 -
     1.8 -instantiation nat :: bounded_forall
     1.9 -begin
    1.10 -
    1.11 -fun bounded_forall_nat :: "(nat => bool) => code_numeral => bool"
    1.12 -where
    1.13 -  "bounded_forall P d = ((P 0) \<and> (if d > 0 then bounded_forall (%n. P (Suc n)) (d - 1) else True))"
    1.14 -
    1.15 -instance ..
    1.16 -
    1.17 -end
    1.18 -
    1.19  subsection {* Defining combinators for any first-order data type *}
    1.20  
    1.21  definition catch_match :: "term list option => term list option => term list option"