  The use of a functional language to implement proof strategies as proof
tactics in interactive theorem provers, often provides short, concise and
elegant implementations. Whilst being elegant, the use of higher order features
and combinator languages often results in a very procedural view of a strategy,
which may deviate significantly from the high-level ideas behind it. This can
make a tactic hard to understand and hence difficult to to debug and maintain
for experts and non-experts alike: one often has to tear apart complex
combinations of lower level tactics manually in order to analyse a failure in
the overall strategy. In an industrial technology transfer project, we have
been working on porting a very large and complex proof tactic into PSGraph, a
graphical language for representing proof strategies, supported by the Tinker
tool. The goal of this work is to improve understandability and maintainability
of tactics. Motivated by some initial successes with this, we here extend
PSGraph with additional features for development and debugging. Through the
re-implementation and refactoring of several existing tactics, we demonstrates
the advantages of PSGraph compared with a typical linear (term-based) tactic
language with respect to debugging, readability and maintenance. In order to
act as guidance for others, we give a fairly detailed comparison of the user
experience with the two approaches. The paper is supported by a web page
providing further details about the implementation as well as interactive
illustrations of the examples.
