changeset 19835 | 81d6dc597559 |
parent 19174 | df9de25e87b3 |
child 21246 | e0e555b67fe5 |
--- a/src/HOL/ROOT.ML Fri Jun 09 17:32:38 2006 +0200 +++ b/src/HOL/ROOT.ML Sun Jun 11 00:28:18 2006 +0200 @@ -13,6 +13,10 @@ use "~~/src/Provers/splitter.ML"; use "~~/src/Provers/hypsubst.ML"; +use "~~/src/Provers/IsaPlanner/zipper.ML"; +use "~~/src/Provers/IsaPlanner/isand.ML"; +use "~~/src/Provers/IsaPlanner/rw_tools.ML"; +use "~~/src/Provers/IsaPlanner/rw_inst.ML"; use "~~/src/Provers/eqsubst.ML"; use "~~/src/Provers/induct_method.ML"; use "~~/src/Provers/classical.ML";