renaming tester from lazy_exhaustive to narrowing
authorbulwahn
Fri Mar 11 15:21:13 2011 +0100 (2011-03-11)
changeset 419369792a882da9c
parent 41935 d786a8a3dc47
child 41937 a369f8ba5425
renaming tester from lazy_exhaustive to narrowing
src/HOL/Tools/Quickcheck/narrowing_generators.ML
     1.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Mar 11 15:21:13 2011 +0100
     1.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Mar 11 15:21:13 2011 +0100
     1.3 @@ -79,7 +79,7 @@
     1.4  structure Counterexample = Proof_Data
     1.5  (
     1.6    type T = unit -> term list option
     1.7 -  fun init _ () = error " Quickcheck_Narrowing_Result"
     1.8 +  fun init _ () = error "Counterexample"
     1.9  )
    1.10  
    1.11  val put_counterexample =  Counterexample.put
    1.12 @@ -99,6 +99,6 @@
    1.13  
    1.14  val setup =
    1.15    Context.theory_map
    1.16 -    (Quickcheck.add_generator ("lazy_exhaustive", compile_generator_expr))
    1.17 +    (Quickcheck.add_generator ("narrowing", compile_generator_expr))
    1.18      
    1.19  end;
    1.20 \ No newline at end of file