We discuss several problems of analogy-driven proof plan construction which prevent a solution for more diæcult target problems or make a solution very expensive. Some of these problems are due to the previously assumed æxed order of matching, reformulation, and replay in case-based reasoning and from a too restricted combination of planning from ærst principles with the analogy process. In order to overcome these problems we suggest to interleave matching and replay as well as casebased planning with planning from ærst principles. Secondly, the restricted mixture of case-based planning and planning from ærst principles in previous systems is generalised to intelligently employing diæerent planning strategies with the objective to solve more problems at all and to solve problems more eæciently.