Things to do in IsaPlanner

Ripple Measure: add submeasures for stuff in wave fronts
Technique Language: distinguish functions from techniques (put techniques into a datatype)
jedit interfaces (or maybe firefox) for working with IsaPlanner
generate Theory files from IsaCoSy and IsaPlanner
use counter-examples to help search for generalisation
Imprve induction technique to use induction schemes from functions, work towards recursion analysis.

Interface

Isar interface for IsaCoSy
A proof plan editor / navigator.
Fix the pretty printing of wave fronts: should just need to modify precedence.
Pretty printing of Meta-variables should ignoring obvious things: arguments that are the same for all meta variables.

A new critic for fertilisation with different associative/commutative operators (like OR, AND etc.) on the top level. Alternatively extend the embedding algorithm to allow embeddings modulo AC.
What to do about the in-progress notion of conjecture in the conjecture database if it has meta variables? We need a meta-variable supporting lookup as well as storing both the initial conjecture without instantiations as well as the instantiated version. Do we also want the inbetween stages?
In Generalisation:
- Improve treatment of Trueprop/bool.
- Imrpove treatment of assumptions: if assumptions included in generalisation, then include them in the conjecture as an assumption. This will allow correct conjectures to be made for proofs about correctness of sorting.

Make the wave-rule database insert the wave-rule theorems into the initial proof-plan. Then, the matching can return a goal-name of the rule instead of the theorem, and the internal version of substitution used. Would be nice (and more efficent) for critics, so they don't have to add every single rule they want to use.
If the above is done, the case-split critic could be made to be a lot nicer, I think the rules for splitting on a true/false condition could be thrown in with the regular wave-rules, and with the new substitution it would be easy to know which goal needs to be proved from conditions, so if this fails we introduce a case-split.
Relational Rippling
Treat the and-choices in rippling correctly to remove symmetries in the search space.
Ripple Measure for middle-out rewriting: Make the measure calculation look back over previous goals when a meta-variable has been instantiated and ensure all steps are still valid measure decreasing ripple steps.
Only recompute ripple-measure for sub-terms that has changed modulo beta-reduction. (I think this had to do with the little loops we get using the sum-of-distance measure.)

Clarity: Provide a better behaved version of unification: one which doesn't introduce renaming instantiations for the target, and which doesn't both introduce and instantiate new variables. (any new variables should not be instantiated - otherwise how can you consider them new???)
Efficiency: Provide multiple simultaneous substitutions. This can be done by having multiple arguments to the outer term used by the substitution tactic.
Utility, Clarity, Efficiency: Instantiation environments should have have both the merge-with-intemediates (currently implemented) as well as a discarding merge (not yet implemented). The discarding merge should throw away intermediate introduced meta variables.
Efficiency, Clarity: Use name-space tables as efficient implementation of sets - allows quicker disjoint checking. Use this to speed up name-disjointness checks and thus (often) avoid extra renaming in rule nets.
Clarity: add flex-flex pair handling to instantiation env.
Efficiency: modify unification/matching etc to give back pairs of ienv, one for target, one for pattern.

Make the string abbriviations for compound methods into real declarative techniques.
Allow resolution to generalise the uninstantiated vars to being new params.
Make real theorems from a proof plan.
Allow parameters to be replaced in subcontexts is the parameter does not occur. This would improve meta-variables in lifted rules getting more parameters than necessary.
Make variable tables hold the real types of variables - not the initial ones. We can then use a correct check for type-equality on variable table merges. -- maybe this isn't needed, in which case we should be using variable name collections - not tables with types.

Allow goal contextual information to have a self-propagation function, so that it automatically updates itself, rather than having to specify the update in a technique.
Allow method-scoped contextual information - contextual information that lives only within the application of a given technique.
Allow contextual information to have an update function for various things, such as instantiation. Does this lead to an event-like model of contextual information? Events in proof planning might want to update contextual information. This is part of the development of sensible dependency management.