# HG changeset patch # User dixon # Date 1149979342 -7200 # Node ID 1704c66e5e7e0b8e8df0b38ba4f49ea64e5d7813 # Parent edc3d1af3b774984158f7aa4f598dcedd6576aa2 updated IsaMakefiles for new location of IsaPlanner. diff -r edc3d1af3b77 -r 1704c66e5e7e src/FOL/IsaMakefile --- a/src/FOL/IsaMakefile Sun Jun 11 00:39:31 2006 +0200 +++ b/src/FOL/IsaMakefile Sun Jun 11 00:42:22 2006 +0200 @@ -30,6 +30,10 @@ $(OUT)/FOL$(ML_SUFFIX): $(OUT)/Pure$(ML_SUFFIX) $(SRC)/Provers/blast.ML \ $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \ + $(SRC)/Provers/IsaPlanner/zipper.ML \ + $(SRC)/Provers/IsaPlanner/isand.ML \ + $(SRC)/Provers/IsaPlanner/rw_tools.ML \ + $(SRC)/Provers/IsaPlanner/rw_inst.ML \ $(SRC)/Provers/eqsubst.ML $(SRC)/Provers/hypsubst.ML \ $(SRC)/Provers/ind.ML $(SRC)/Provers/induct_method.ML \ $(SRC)/Provers/project_rule.ML $(SRC)/Provers/quantifier1.ML \ diff -r edc3d1af3b77 -r 1704c66e5e7e src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Sun Jun 11 00:39:31 2006 +0200 +++ b/src/HOL/IsaMakefile Sun Jun 11 00:42:22 2006 +0200 @@ -72,6 +72,10 @@ $(SRC)/Provers/Arith/extract_common_term.ML \ $(SRC)/Provers/Arith/fast_lin_arith.ML $(SRC)/Provers/blast.ML \ $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \ + $(SRC)/Provers/IsaPlanner/zipper.ML \ + $(SRC)/Provers/IsaPlanner/isand.ML \ + $(SRC)/Provers/IsaPlanner/rw_tools.ML \ + $(SRC)/Provers/IsaPlanner/rw_inst.ML \ $(SRC)/Provers/eqsubst.ML $(SRC)/Provers/hypsubst.ML \ $(SRC)/Provers/induct_method.ML $(SRC)/Provers/order.ML \ $(SRC)/Provers/project_rule.ML $(SRC)/Provers/quantifier1.ML \