correcting dependencies after renaming
authorbulwahn
Fri, 11 Mar 2011 15:21:13 +0100
changeset 41919 e180c2a9873b
parent 41918 d2ab869f8b0b
child 41920 d4fb7a418152
correcting dependencies after renaming
src/HOL/IsaMakefile
src/HOL/Main.thy
--- 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 \
--- 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 {*