Matita is a proof assistant characterised by a rich, user extensible, output facility based on a widget for the rendering
of MathML Presentation, and by the automatic handling of overloading by means of a flexible disambiguation mechanism. We show
how to use these features to obtain a simple learning environment for natural deduction, without modifying the source code
or Matita.