tuned headers -- adapted to usual conventions;
authorwenzelm
Thu May 31 21:09:14 2007 +0200 (2007-05-31)
changeset 23175267ba70e7a9d
parent 23174 3913451b0418
child 23176 40a760921d94
tuned headers -- adapted to usual conventions;
src/Tools/IsaPlanner/isand.ML
src/Tools/IsaPlanner/rw_inst.ML
src/Tools/IsaPlanner/rw_tools.ML
src/Tools/IsaPlanner/zipper.ML
     1.1 --- a/src/Tools/IsaPlanner/isand.ML	Thu May 31 20:55:33 2007 +0200
     1.2 +++ b/src/Tools/IsaPlanner/isand.ML	Thu May 31 21:09:14 2007 +0200
     1.3 @@ -1,32 +1,25 @@
     1.4 -(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
     1.5 -(*  Title:      Pure/IsaPlanner/isand.ML
     1.6 +(*  Title:      Tools/IsaPlanner/isand.ML
     1.7      ID:		$Id$
     1.8      Author:     Lucas Dixon, University of Edinburgh
     1.9 -                lucas.dixon@ed.ac.uk
    1.10 -    Updated:    26 Apr 2005
    1.11 -    Date:       6 Aug 2004
    1.12 -*)
    1.13 -(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
    1.14 -(*  DESCRIPTION:
    1.15 +
    1.16 +Natural Deduction tools.
    1.17  
    1.18 -    Natural Deduction tools
    1.19 +For working with Isabelle theorems in a natural detuction style.
    1.20 +ie, not having to deal with meta level quantified varaibles,
    1.21 +instead, we work with newly introduced frees, and hide the
    1.22 +"all"'s, exporting results from theorems proved with the frees, to
    1.23 +solve the all cases of the previous goal. This allows resolution
    1.24 +to do proof search normally. 
    1.25  
    1.26 -    For working with Isabelle theorems in a natural detuction style.
    1.27 -    ie, not having to deal with meta level quantified varaibles,
    1.28 -    instead, we work with newly introduced frees, and hide the
    1.29 -    "all"'s, exporting results from theorems proved with the frees, to
    1.30 -    solve the all cases of the previous goal. This allows resolution
    1.31 -    to do proof search normally. 
    1.32 +Note: A nice idea: allow exporting to solve any subgoal, thus
    1.33 +allowing the interleaving of proof, or provide a structure for the
    1.34 +ordering of proof, thus allowing proof attempts in parrell, but
    1.35 +recording the order to apply things in.
    1.36  
    1.37 -    Note: A nice idea: allow exporting to solve any subgoal, thus
    1.38 -    allowing the interleaving of proof, or provide a structure for the
    1.39 -    ordering of proof, thus allowing proof attempts in parrell, but
    1.40 -    recording the order to apply things in.
    1.41 -
    1.42 -    THINK: are we really ok with our varify name w.r.t the prop - do
    1.43 -    we also need to avoid names in the hidden hyps? What about
    1.44 -    unification contraints in flex-flex pairs - might they also have
    1.45 -    extra free vars?
    1.46 +THINK: are we really ok with our varify name w.r.t the prop - do
    1.47 +we also need to avoid names in the hidden hyps? What about
    1.48 +unification contraints in flex-flex pairs - might they also have
    1.49 +extra free vars?
    1.50  *)
    1.51  
    1.52  signature ISA_ND =
     2.1 --- a/src/Tools/IsaPlanner/rw_inst.ML	Thu May 31 20:55:33 2007 +0200
     2.2 +++ b/src/Tools/IsaPlanner/rw_inst.ML	Thu May 31 21:09:14 2007 +0200
     2.3 @@ -1,18 +1,11 @@
     2.4 -(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
     2.5 -(*  Title:      Pure/IsaPlanner/rw_inst.ML
     2.6 +(*  Title:      Tools/IsaPlanner/rw_inst.ML
     2.7      ID:         $Id$
     2.8      Author:     Lucas Dixon, University of Edinburgh
     2.9 -                lucas.dixon@ed.ac.uk
    2.10 -    Created:    25 Aug 2004
    2.11 -*)
    2.12 -(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
    2.13 -(*  DESCRIPTION:
    2.14  
    2.15 -    rewriting using a conditional meta-equality theorem which supports 
    2.16 -    schematic variable instantiation.
    2.17 +Rewriting using a conditional meta-equality theorem which supports
    2.18 +schematic variable instantiation.
    2.19 +*)   
    2.20  
    2.21 -*)   
    2.22 -(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
    2.23  signature RW_INST =
    2.24  sig
    2.25  
     3.1 --- a/src/Tools/IsaPlanner/rw_tools.ML	Thu May 31 20:55:33 2007 +0200
     3.2 +++ b/src/Tools/IsaPlanner/rw_tools.ML	Thu May 31 21:09:14 2007 +0200
     3.3 @@ -1,17 +1,9 @@
     3.4 -(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
     3.5 -(*  Title:      Pure/IsaPlanner/rw_tools.ML
     3.6 +(*  Title:      Tools/IsaPlanner/rw_tools.ML
     3.7      ID:		$Id$
     3.8      Author:     Lucas Dixon, University of Edinburgh
     3.9 -                lucas.dixon@ed.ac.uk
    3.10 -    Created:    28 May 2004
    3.11 -*)
    3.12 -(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
    3.13 -(*  DESCRIPTION:
    3.14  
    3.15 -    term related tools used for rewriting
    3.16 -
    3.17 +Term related tools used for rewriting.
    3.18  *)   
    3.19 -(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
    3.20  
    3.21  signature RWTOOLS =
    3.22  sig
     4.1 --- a/src/Tools/IsaPlanner/zipper.ML	Thu May 31 20:55:33 2007 +0200
     4.2 +++ b/src/Tools/IsaPlanner/zipper.ML	Thu May 31 21:09:14 2007 +0200
     4.3 @@ -1,17 +1,10 @@
     4.4 -(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
     4.5 -(*  Title:      Pure/IsaPlanner/zipper.ML
     4.6 +(*  Title:      Tools/IsaPlanner/zipper.ML
     4.7      ID:		$Id$
     4.8      Author:     Lucas Dixon, University of Edinburgh
     4.9 -                lucas.dixon@ed.ac.uk
    4.10 -    Created:    24 Mar 2006
    4.11 -*)
    4.12 -(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
    4.13 -(*  DESCRIPTION:
    4.14 -    A notion roughly based on Huet's Zippers for Isabelle terms.
    4.15 +
    4.16 +A notion roughly based on Huet's Zippers for Isabelle terms.
    4.17  *)   
    4.18  
    4.19 -(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
    4.20 -
    4.21  (* abstract term for no more than pattern matching *)
    4.22  signature ABSTRACT_TRM = 
    4.23  sig