# HG changeset patch
# User bulwahn
# Date 1302273074 -7200
# Node ID 494c31fdec9577ae1cd341e834e114cc37382ee2
# Parent  34366f39d32d6bf784d4e0ad85f4ad9c688084ef
theory definitions for fast exhaustive quickcheck compilation

diff -r 34366f39d32d -r 494c31fdec95 src/HOL/Quickcheck_Exhaustive.thy
--- a/src/HOL/Quickcheck_Exhaustive.thy	Fri Apr 08 16:31:14 2011 +0200
+++ b/src/HOL/Quickcheck_Exhaustive.thy	Fri Apr 08 16:31:14 2011 +0200
@@ -390,6 +390,20 @@
 class bounded_forall =
   fixes bounded_forall :: "('a \<Rightarrow> bool) \<Rightarrow> code_numeral \<Rightarrow> bool"
 
+subsection {* Fast exhaustive combinators *}
+
+
+class fast_exhaustive = term_of +
+  fixes fast_exhaustive :: "('a \<Rightarrow> unit) \<Rightarrow> code_numeral \<Rightarrow> unit"
+
+consts throw_Counterexample :: "term list => unit"
+consts catch_Counterexample :: "unit => term list option"
+
+code_const throw_Counterexample
+  (Quickcheck "raise (Exhaustive'_Generators.Counterexample _)")
+code_const catch_Counterexample
+  (Quickcheck "(((_); NONE) handle Exhaustive'_Generators.Counterexample ts => SOME ts)")
+
 subsection {* Defining combinators for any first-order data type *}
 
 definition catch_match :: "term list option => term list option => term list option"