# HG changeset patch
# User wenzelm
# Date 1180637731 -7200
# Node ID f1ae6a8648ef054cc036e6b59d5b2136dc9bbe12
# Parent  861f63a35d31cb084922727e4858801a1f6cf96f
moved IsaPlanner from Provers to Tools;
moved Compute_Oracle from Pure/Tools to Tools;

diff -r 861f63a35d31 -r f1ae6a8648ef src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Thu May 31 20:55:29 2007 +0200
+++ b/src/HOL/IsaMakefile	Thu May 31 20:55:31 2007 +0200
@@ -71,10 +71,10 @@
   $(SRC)/Provers/Arith/combine_numerals.ML					\
   $(SRC)/Provers/Arith/extract_common_term.ML					\
   $(SRC)/Provers/Arith/fast_lin_arith.ML					\
-  $(SRC)/Provers/IsaPlanner/isand.ML						\
-  $(SRC)/Provers/IsaPlanner/rw_inst.ML						\
-  $(SRC)/Provers/IsaPlanner/rw_tools.ML						\
-  $(SRC)/Provers/IsaPlanner/zipper.ML $(SRC)/Provers/blast.ML			\
+  $(SRC)/Tools/IsaPlanner/isand.ML						\
+  $(SRC)/Tools/IsaPlanner/rw_inst.ML						\
+  $(SRC)/Tools/IsaPlanner/rw_tools.ML						\
+  $(SRC)/Tools/IsaPlanner/zipper.ML $(SRC)/Provers/blast.ML			\
   $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML				\
   $(SRC)/Provers/eqsubst.ML $(SRC)/Provers/hypsubst.ML				\
   $(SRC)/Provers/induct_method.ML $(SRC)/Provers/order.ML			\
@@ -678,8 +678,12 @@
 HOL-Complex-Matrix: HOL-Complex $(OUT)/HOL-Complex-Matrix
 
 $(OUT)/HOL-Complex-Matrix: $(OUT)/HOL-Complex \
-  Matrix/MatrixGeneral.thy Matrix/Matrix.thy Matrix/SparseMatrix.thy Matrix/LP.thy \
-  Matrix/document/root.tex Matrix/ROOT.ML \
+  $(SRC)/Tools/Compute_Oracle/Compute_Oracle.thy \
+  $(SRC)/Tools/Compute_Oracle/am_compiler.ML \
+  $(SRC)/Tools/Compute_Oracle/am_interpreter.ML \
+  $(SRC)/Tools/Compute_Oracle/am_util.ML $(SRC)/Tools/Compute_Oracle/compute.ML \
+  Matrix/MatrixGeneral.thy Matrix/Matrix.thy Matrix/SparseMatrix.thy \
+  Matrix/LP.thy Matrix/document/root.tex Matrix/ROOT.ML \
   Matrix/cplex/Cplex.thy Matrix/cplex/CplexMatrixConverter.ML \
   Matrix/cplex/Cplex_tools.ML Matrix/cplex/FloatSparseMatrix.thy \
   Matrix/cplex/FloatSparseMatrixBuilder.ML Matrix/cplex/fspmlp.ML \