--- a/src/HOL/Quickcheck_Exhaustive.thy Tue Apr 05 08:53:52 2011 +0200
+++ b/src/HOL/Quickcheck_Exhaustive.thy Tue Apr 05 09:38:23 2011 +0200
@@ -360,18 +360,6 @@
class bounded_forall =
fixes bounded_forall :: "('a \<Rightarrow> bool) \<Rightarrow> code_numeral \<Rightarrow> bool"
-
-instantiation nat :: bounded_forall
-begin
-
-fun bounded_forall_nat :: "(nat => bool) => code_numeral => bool"
-where
- "bounded_forall P d = ((P 0) \<and> (if d > 0 then bounded_forall (%n. P (Suc n)) (d - 1) else True))"
-
-instance ..
-
-end
-
subsection {* Defining combinators for any first-order data type *}
definition catch_match :: "term list option => term list option => term list option"