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