renaming tester from lazy_exhaustive to narrowing
authorbulwahn
Fri, 11 Mar 2011 15:21:13 +0100
changeset 41936 9792a882da9c
parent 41935 d786a8a3dc47
child 41937 a369f8ba5425
renaming tester from lazy_exhaustive to narrowing
src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Mar 11 15:21:13 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Mar 11 15:21:13 2011 +0100
@@ -79,7 +79,7 @@
 structure Counterexample = Proof_Data
 (
   type T = unit -> term list option
-  fun init _ () = error " Quickcheck_Narrowing_Result"
+  fun init _ () = error "Counterexample"
 )
 
 val put_counterexample =  Counterexample.put
@@ -99,6 +99,6 @@
 
 val setup =
   Context.theory_map
-    (Quickcheck.add_generator ("lazy_exhaustive", compile_generator_expr))
+    (Quickcheck.add_generator ("narrowing", compile_generator_expr))
     
 end;
\ No newline at end of file