src/Provers/IsaPlanner/ROOT.ML

Reimplemented algebra method; now controlled by attribute.

(*  ID:         $Id$
    Author:     Lucas Dixon, University of Edinburgh
                [e-mail]

The IsaPlanner subsystem.
*)

(* Generic notion of term Zippers *)
use "zipper.ML";

(* Some tools for manipulation of proofs following a ND style *)
use "isand.ML";

(* some tools for rewriting *)
use "rw_tools.ML";
use "rw_inst.ML";