making active configuration public in narrowing-based quickcheck
authorbulwahn
Mon, 18 Jul 2011 13:48:35 +0200
changeset 43891 4690f76f327a
parent 43890 eba9c3b1f84a
child 43892 86ede854b4f5
making active configuration public in narrowing-based quickcheck
src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon Jul 18 11:38:14 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon Jul 18 13:48:35 2011 +0200
@@ -9,6 +9,7 @@
   val allow_existentials : bool Config.T
   val finite_functions : bool Config.T
   val overlord : bool Config.T
+  val active : bool Config.T
   val test_term: Proof.context -> bool * bool -> term * term list -> Quickcheck.result
   datatype counterexample = Universal_Counterexample of (term * counterexample)
     | Existential_Counterexample of (term * counterexample) list