Abstract
This report describes some of the technology used to build a user interface for a programmable theorem prover. By separating the user interface from the application itself, it is possible to experiment with new interface features very easily, without compromising the soundness of the proof tool.