src/HOL/Tools/Quickcheck/narrowing_generators.ML
changeset 43891 4690f76f327a
parent 43878 eeb10fdd9535
child 43892 86ede854b4f5
     1.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon Jul 18 11:38:14 2011 +0200
     1.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon Jul 18 13:48:35 2011 +0200
     1.3 @@ -9,6 +9,7 @@
     1.4    val allow_existentials : bool Config.T
     1.5    val finite_functions : bool Config.T
     1.6    val overlord : bool Config.T
     1.7 +  val active : bool Config.T
     1.8    val test_term: Proof.context -> bool * bool -> term * term list -> Quickcheck.result
     1.9    datatype counterexample = Universal_Counterexample of (term * counterexample)
    1.10      | Existential_Counterexample of (term * counterexample) list