User modeling research can benefit from formal automated reasoning tools. However existing formal tools may need to be modified to suit the needs of user modeling. Theorist is a simple framework for default reasoning. It can be used as a tool for building and maintaining a user model, and as a model of a user's default reasoning. To apply Theorist to both tasks, we develop Nested Theorist (NT), a simple tool based on Theorist that allows default reasoning on arbitrarily-many levels. We extend NT in two ways: we allow prioritized defaults, and we allow reasoning about agents with limited reasoning capabilities. This paper focusses on applications, and uses wide-ranging examples from user-modeling literature to illustrate the usefulness of the tools presented.