src/HOL/Quickcheck_Exhaustive.thy
changeset 41918 d2ab869f8b0b
parent 41916 80060d5f864a
child 41920 d4fb7a418152
     1.1 --- a/src/HOL/Quickcheck_Exhaustive.thy	Fri Mar 11 15:21:13 2011 +0100
     1.2 +++ b/src/HOL/Quickcheck_Exhaustive.thy	Fri Mar 11 15:21:13 2011 +0100
     1.3 @@ -2,7 +2,7 @@
     1.4  
     1.5  header {* A simple counterexample generator performing exhaustive testing *}
     1.6  
     1.7 -theory Quickcheck_Exhautive
     1.8 +theory Quickcheck_Exhaustive
     1.9  imports Quickcheck
    1.10  uses ("Tools/exhaustive_generators.ML")
    1.11  begin
    1.12 @@ -368,9 +368,9 @@
    1.13  code_const catch_match 
    1.14    (SML "(_) handle Match => _")
    1.15  
    1.16 -use "Tools/smallvalue_generators.ML"
    1.17 +use "Tools/exhaustive_generators.ML"
    1.18  
    1.19 -setup {* Smallvalue_Generators.setup *}
    1.20 +setup {* Exhaustive_Generators.setup *}
    1.21  
    1.22  declare [[quickcheck_tester = exhaustive]]
    1.23