# HG changeset patch
# User bulwahn
# Date 1299853273 -3600
# Node ID e180c2a9873bf8c32fc8ba8ed0ffc76adf518013
# Parent  d2ab869f8b0b6acbdfe13bdc75ed5189e5ffbe2b
correcting dependencies after renaming

diff -r d2ab869f8b0b -r e180c2a9873b src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri Mar 11 15:21:13 2011 +0100
+++ b/src/HOL/IsaMakefile	Fri Mar 11 15:21:13 2011 +0100
@@ -276,6 +276,7 @@
   Presburger.thy \
   Predicate_Compile.thy \
   Quickcheck.thy \
+  Quickcheck_Exhaustive.thy \
   Quotient.thy \
   Random.thy \
   Random_Sequence.thy \
@@ -285,7 +286,6 @@
   Semiring_Normalization.thy \
   SetInterval.thy \
   Sledgehammer.thy \
-  Smallcheck.thy \
   SMT.thy \
   String.thy \
   Typerep.thy \
@@ -299,8 +299,9 @@
   Tools/ATP/atp_systems.ML \
   Tools/choice_specification.ML \
   Tools/code_evaluation.ML \
+  Tools/exhaustive_generators.ML \
+  Tools/groebner.ML \
   Tools/int_arith.ML \
-  Tools/groebner.ML \
   Tools/list_code.ML \
   Tools/list_to_set_comprehension.ML \
   Tools/nat_numeral_simprocs.ML \
@@ -354,7 +355,6 @@
   Tools/Sledgehammer/sledgehammer_provers.ML \
   Tools/Sledgehammer/sledgehammer_run.ML \
   Tools/Sledgehammer/sledgehammer_util.ML \
-  Tools/smallvalue_generators.ML \
   Tools/SMT/smtlib_interface.ML \
   Tools/SMT/smt_builtin.ML \
   Tools/SMT/smt_config.ML \
diff -r d2ab869f8b0b -r e180c2a9873b src/HOL/Main.thy
--- a/src/HOL/Main.thy	Fri Mar 11 15:21:13 2011 +0100
+++ b/src/HOL/Main.thy	Fri Mar 11 15:21:13 2011 +0100
@@ -1,7 +1,7 @@
 header {* Main HOL *}
 
 theory Main
-imports Plain Record Predicate_Compile Smallcheck Nitpick
+imports Plain Record Predicate_Compile Quickcheck_Exhaustive Nitpick
 begin
 
 text {*