src/Provers/IsaPlanner/ROOT.ML
author wenzelm
Thu Dec 07 00:42:04 2006 +0100 (2006-12-07)
changeset 21687 f689f729afab
parent 19835 81d6dc597559
permissions -rw-r--r--
reorganized structure Goal vs. Tactic;
dixon@19835
     1
(*  ID:         $Id$
dixon@19835
     2
    Author:     Lucas Dixon, University of Edinburgh
dixon@19835
     3
                lucas.dixon@ed.ac.uk
dixon@19835
     4
dixon@19835
     5
The IsaPlanner subsystem.
dixon@19835
     6
*)
dixon@19835
     7
dixon@19835
     8
(* Generic notion of term Zippers *)
dixon@19835
     9
use "zipper.ML";
dixon@19835
    10
dixon@19835
    11
(* Some tools for manipulation of proofs following a ND style *)
dixon@19835
    12
use "isand.ML";
dixon@19835
    13
dixon@19835
    14
(* some tools for rewriting *)
dixon@19835
    15
use "rw_tools.ML";
dixon@19835
    16
use "rw_inst.ML";