src/HOL/Quickcheck_Exhaustive.thy

 (* Author: Lukas Bulwahn, TU Muenchen *)
 
 header {* A simple counterexample generator performing exhaustive testing *}
 
-theory Quickcheck_Exhautive
+theory Quickcheck_Exhaustive
 imports Quickcheck
 uses ("Tools/exhaustive_generators.ML")
 begin
 
 subsection {* basic operations for exhaustive generators *}

   [code del]: "catch_match t1 t2 = (SOME t. t = t1 \<or> t = t2)"
 
 code_const catch_match 
   (SML "(_) handle Match => _")
 
-use "Tools/smallvalue_generators.ML"
-
-setup {* Smallvalue_Generators.setup *}
+use "Tools/exhaustive_generators.ML"
+
+setup {* Exhaustive_Generators.setup *}
 
 declare [[quickcheck_tester = exhaustive]]
 
 hide_fact orelse_def catch_match_def
 no_notation orelse (infixr "orelse" 55)