# HG changeset patch
# User wenzelm
# Date 1180638554 -7200
# Node ID 267ba70e7a9dcab574c7b9dd861a75a3f5f19898
# Parent  3913451b04181b56c97afb5abecdeafdcd38103e
tuned headers -- adapted to usual conventions;

diff -r 3913451b0418 -r 267ba70e7a9d src/Tools/IsaPlanner/isand.ML
--- a/src/Tools/IsaPlanner/isand.ML	Thu May 31 20:55:33 2007 +0200
+++ b/src/Tools/IsaPlanner/isand.ML	Thu May 31 21:09:14 2007 +0200
@@ -1,32 +1,25 @@
-(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
-(*  Title:      Pure/IsaPlanner/isand.ML
+(*  Title:      Tools/IsaPlanner/isand.ML
     ID:		$Id$
     Author:     Lucas Dixon, University of Edinburgh
-                lucas.dixon@ed.ac.uk
-    Updated:    26 Apr 2005
-    Date:       6 Aug 2004
-*)
-(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
-(*  DESCRIPTION:
+
+Natural Deduction tools.
 
-    Natural Deduction tools
+For working with Isabelle theorems in a natural detuction style.
+ie, not having to deal with meta level quantified varaibles,
+instead, we work with newly introduced frees, and hide the
+"all"'s, exporting results from theorems proved with the frees, to
+solve the all cases of the previous goal. This allows resolution
+to do proof search normally. 
 
-    For working with Isabelle theorems in a natural detuction style.
-    ie, not having to deal with meta level quantified varaibles,
-    instead, we work with newly introduced frees, and hide the
-    "all"'s, exporting results from theorems proved with the frees, to
-    solve the all cases of the previous goal. This allows resolution
-    to do proof search normally. 
+Note: A nice idea: allow exporting to solve any subgoal, thus
+allowing the interleaving of proof, or provide a structure for the
+ordering of proof, thus allowing proof attempts in parrell, but
+recording the order to apply things in.
 
-    Note: A nice idea: allow exporting to solve any subgoal, thus
-    allowing the interleaving of proof, or provide a structure for the
-    ordering of proof, thus allowing proof attempts in parrell, but
-    recording the order to apply things in.
-
-    THINK: are we really ok with our varify name w.r.t the prop - do
-    we also need to avoid names in the hidden hyps? What about
-    unification contraints in flex-flex pairs - might they also have
-    extra free vars?
+THINK: are we really ok with our varify name w.r.t the prop - do
+we also need to avoid names in the hidden hyps? What about
+unification contraints in flex-flex pairs - might they also have
+extra free vars?
 *)
 
 signature ISA_ND =
diff -r 3913451b0418 -r 267ba70e7a9d src/Tools/IsaPlanner/rw_inst.ML
--- a/src/Tools/IsaPlanner/rw_inst.ML	Thu May 31 20:55:33 2007 +0200
+++ b/src/Tools/IsaPlanner/rw_inst.ML	Thu May 31 21:09:14 2007 +0200
@@ -1,18 +1,11 @@
-(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
-(*  Title:      Pure/IsaPlanner/rw_inst.ML
+(*  Title:      Tools/IsaPlanner/rw_inst.ML
     ID:         $Id$
     Author:     Lucas Dixon, University of Edinburgh
-                lucas.dixon@ed.ac.uk
-    Created:    25 Aug 2004
-*)
-(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
-(*  DESCRIPTION:
 
-    rewriting using a conditional meta-equality theorem which supports 
-    schematic variable instantiation.
+Rewriting using a conditional meta-equality theorem which supports
+schematic variable instantiation.
+*)   
 
-*)   
-(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
 signature RW_INST =
 sig
 
diff -r 3913451b0418 -r 267ba70e7a9d src/Tools/IsaPlanner/rw_tools.ML
--- a/src/Tools/IsaPlanner/rw_tools.ML	Thu May 31 20:55:33 2007 +0200
+++ b/src/Tools/IsaPlanner/rw_tools.ML	Thu May 31 21:09:14 2007 +0200
@@ -1,17 +1,9 @@
-(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
-(*  Title:      Pure/IsaPlanner/rw_tools.ML
+(*  Title:      Tools/IsaPlanner/rw_tools.ML
     ID:		$Id$
     Author:     Lucas Dixon, University of Edinburgh
-                lucas.dixon@ed.ac.uk
-    Created:    28 May 2004
-*)
-(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
-(*  DESCRIPTION:
 
-    term related tools used for rewriting
-
+Term related tools used for rewriting.
 *)   
-(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
 
 signature RWTOOLS =
 sig
diff -r 3913451b0418 -r 267ba70e7a9d src/Tools/IsaPlanner/zipper.ML
--- a/src/Tools/IsaPlanner/zipper.ML	Thu May 31 20:55:33 2007 +0200
+++ b/src/Tools/IsaPlanner/zipper.ML	Thu May 31 21:09:14 2007 +0200
@@ -1,17 +1,10 @@
-(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
-(*  Title:      Pure/IsaPlanner/zipper.ML
+(*  Title:      Tools/IsaPlanner/zipper.ML
     ID:		$Id$
     Author:     Lucas Dixon, University of Edinburgh
-                lucas.dixon@ed.ac.uk
-    Created:    24 Mar 2006
-*)
-(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
-(*  DESCRIPTION:
-    A notion roughly based on Huet's Zippers for Isabelle terms.
+
+A notion roughly based on Huet's Zippers for Isabelle terms.
 *)   
 
-(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
-
 (* abstract term for no more than pattern matching *)
 signature ABSTRACT_TRM = 
 sig