# HG changeset patch
# User blanchet
# Date 1309969174 -3600
# Node ID c00febb8e39c60245eda141629238c4fd65253fb
# Parent  92f78a4a5628ad1f6fc10400c3564016c014fa67
moved ATP dependencies to HOL-Plain, where they belong

diff -r 92f78a4a5628 -r c00febb8e39c src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Wed Jul 06 17:19:34 2011 +0100
+++ b/src/HOL/IsaMakefile	Wed Jul 06 17:19:34 2011 +0100
@@ -169,6 +169,7 @@
   $(SRC)/Provers/trancl.ML \
   $(SRC)/Tools/Metis/metis.ML \
   $(SRC)/Tools/rat.ML \
+  ATP.thy \
   Complete_Lattice.thy \
   Complete_Partial_Order.thy \
   Datatype.thy \
@@ -195,6 +196,12 @@
   SAT.thy \
   Set.thy \
   Sum_Type.thy \
+  Tools/ATP/atp_problem.ML \
+  Tools/ATP/atp_proof.ML \
+  Tools/ATP/atp_reconstruct.ML \
+  Tools/ATP/atp_systems.ML \
+  Tools/ATP/atp_translate.ML \
+  Tools/ATP/atp_util.ML \
   Tools/Datatype/datatype.ML \
   Tools/Datatype/datatype_abs_proofs.ML \
   Tools/Datatype/datatype_aux.ML \
@@ -256,7 +263,6 @@
 	@$(ISABELLE_TOOL) usedir -b -f plain.ML -g true $(OUT)/Pure HOL-Plain
 
 MAIN_DEPENDENCIES = $(PLAIN_DEPENDENCIES) \
-  ATP.thy \
   Big_Operators.thy \
   Code_Evaluation.thy \
   Code_Numeral.thy \
@@ -299,12 +305,6 @@
   $(SRC)/Provers/Arith/cancel_numerals.ML \
   $(SRC)/Provers/Arith/combine_numerals.ML \
   $(SRC)/Provers/Arith/extract_common_term.ML \
-  Tools/ATP/atp_problem.ML \
-  Tools/ATP/atp_proof.ML \
-  Tools/ATP/atp_reconstruct.ML \
-  Tools/ATP/atp_systems.ML \
-  Tools/ATP/atp_translate.ML \
-  Tools/ATP/atp_util.ML \
   Tools/choice_specification.ML \
   Tools/code_evaluation.ML \
   Tools/groebner.ML \