The Lübeck Transformation System supports the refinement of higher order algebraic specifications following sound transformation rules. We discuss the system requirements, describe the specification language and explain the life cycle of a specification in the transformation process. The system analyses various properties of the specification providing user guidance for further design decisions. The refinement relation is implemented by two refinement modes covering the different transformation rules for entire specifications and single axioms. Finally we describe the architecture and the implementation of the system. Throughout the paper, we accompany the presentation with a running example.