moved IsaPlanner from Provers to Tools;
authorwenzelm
Thu May 31 20:55:31 2007 +0200 (2007-05-31)
changeset 23172f1ae6a8648ef
parent 23171 861f63a35d31
child 23173 51179ca0c429
moved IsaPlanner from Provers to Tools;
moved Compute_Oracle from Pure/Tools to Tools;
src/HOL/IsaMakefile
     1.1 --- a/src/HOL/IsaMakefile	Thu May 31 20:55:29 2007 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Thu May 31 20:55:31 2007 +0200
     1.3 @@ -71,10 +71,10 @@
     1.4    $(SRC)/Provers/Arith/combine_numerals.ML					\
     1.5    $(SRC)/Provers/Arith/extract_common_term.ML					\
     1.6    $(SRC)/Provers/Arith/fast_lin_arith.ML					\
     1.7 -  $(SRC)/Provers/IsaPlanner/isand.ML						\
     1.8 -  $(SRC)/Provers/IsaPlanner/rw_inst.ML						\
     1.9 -  $(SRC)/Provers/IsaPlanner/rw_tools.ML						\
    1.10 -  $(SRC)/Provers/IsaPlanner/zipper.ML $(SRC)/Provers/blast.ML			\
    1.11 +  $(SRC)/Tools/IsaPlanner/isand.ML						\
    1.12 +  $(SRC)/Tools/IsaPlanner/rw_inst.ML						\
    1.13 +  $(SRC)/Tools/IsaPlanner/rw_tools.ML						\
    1.14 +  $(SRC)/Tools/IsaPlanner/zipper.ML $(SRC)/Provers/blast.ML			\
    1.15    $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML				\
    1.16    $(SRC)/Provers/eqsubst.ML $(SRC)/Provers/hypsubst.ML				\
    1.17    $(SRC)/Provers/induct_method.ML $(SRC)/Provers/order.ML			\
    1.18 @@ -678,8 +678,12 @@
    1.19  HOL-Complex-Matrix: HOL-Complex $(OUT)/HOL-Complex-Matrix
    1.20  
    1.21  $(OUT)/HOL-Complex-Matrix: $(OUT)/HOL-Complex \
    1.22 -  Matrix/MatrixGeneral.thy Matrix/Matrix.thy Matrix/SparseMatrix.thy Matrix/LP.thy \
    1.23 -  Matrix/document/root.tex Matrix/ROOT.ML \
    1.24 +  $(SRC)/Tools/Compute_Oracle/Compute_Oracle.thy \
    1.25 +  $(SRC)/Tools/Compute_Oracle/am_compiler.ML \
    1.26 +  $(SRC)/Tools/Compute_Oracle/am_interpreter.ML \
    1.27 +  $(SRC)/Tools/Compute_Oracle/am_util.ML $(SRC)/Tools/Compute_Oracle/compute.ML \
    1.28 +  Matrix/MatrixGeneral.thy Matrix/Matrix.thy Matrix/SparseMatrix.thy \
    1.29 +  Matrix/LP.thy Matrix/document/root.tex Matrix/ROOT.ML \
    1.30    Matrix/cplex/Cplex.thy Matrix/cplex/CplexMatrixConverter.ML \
    1.31    Matrix/cplex/Cplex_tools.ML Matrix/cplex/FloatSparseMatrix.thy \
    1.32    Matrix/cplex/FloatSparseMatrixBuilder.ML Matrix/cplex/fspmlp.ML \