summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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 =