renamed generator into exhaustive
authorbulwahn
Fri Dec 03 08:40:47 2010 +0100 (2010-12-03)
changeset 4091399a4ef20704d
parent 40912 1108529100ce
child 40914 0c071c5202b5
renamed generator into exhaustive
src/HOL/Tools/smallvalue_generators.ML
     1.1 --- a/src/HOL/Tools/smallvalue_generators.ML	Fri Dec 03 08:40:47 2010 +0100
     1.2 +++ b/src/HOL/Tools/smallvalue_generators.ML	Fri Dec 03 08:40:47 2010 +0100
     1.3 @@ -289,6 +289,6 @@
     1.4      (Quickcheck_Generators.ensure_sort_datatype (@{sort full_small}, instantiate_smallvalue_datatype))
     1.5    #> setup_smart_quantifier
     1.6    #> Context.theory_map
     1.7 -    (Quickcheck.add_generator ("small", compile_generator_expr));
     1.8 +    (Quickcheck.add_generator ("exhaustive", compile_generator_expr));
     1.9  
    1.10  end;