src/Tools/quickcheck.ML
changeset 43883 aacbe67793c3
parent 43882 05d5696f177f
child 43884 59ba3dbd1400
--- a/src/Tools/quickcheck.ML	Mon Jul 18 10:34:21 2011 +0200
+++ b/src/Tools/quickcheck.ML	Mon Jul 18 10:34:21 2011 +0200
@@ -63,7 +63,8 @@
     Proof.context -> bool * bool -> (string * typ) list -> (term * term list) list -> result list
   (* testing terms and proof states *)
   val test_term: compile_generator -> Proof.context -> bool * bool -> term * term list -> result
-  (*val test_goal_terms : tester*)
+  val test_goal_terms :
+    Proof.context -> bool * bool -> (string * typ) list -> (term * term list) list -> result list option
   val quickcheck: (string * string list) list -> int -> Proof.state -> (string * term) list option
   (* testing a batch of terms *)
   val test_terms: