src/HOL/Quickcheck_Exhaustive.thy
changeset 58813 625d04d4fd2a
parent 58350 919149921e46
child 58826 2ed2eaabe3df
equal deleted inserted replaced
58812:5a9a2d3b9f8b 58813:625d04d4fd2a
   616 
   616 
   617 notation (output) unknown  ("?")
   617 notation (output) unknown  ("?")
   618 
   618 
   619 ML_file "Tools/Quickcheck/exhaustive_generators.ML"
   619 ML_file "Tools/Quickcheck/exhaustive_generators.ML"
   620 
   620 
   621 setup {* Exhaustive_Generators.setup *}
   621 setup Exhaustive_Generators.setup
   622 
   622 
   623 declare [[quickcheck_batch_tester = exhaustive]]
   623 declare [[quickcheck_batch_tester = exhaustive]]
   624 
   624 
   625 subsection {* Defining generators for abstract types *}
   625 subsection {* Defining generators for abstract types *}
   626 
   626