--- 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 =
--- 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
--- 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
--- 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