src/Tools/IsaPlanner/isand.ML
changeset 23175 267ba70e7a9d
parent 23171 861f63a35d31
child 26653 60e0cf6bef89
     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 =