moved IsaPlanner from Provers to Tools;
moved Compute_Oracle from Pure/Tools to Tools;

--- 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 \