Note: this document is part of the earlier Isabelle documentation, which is largely superseded by the Isabelle/HOL Tutorial [9]. It describes the old-style theory syntax and shows how to conduct proofs using the ML top level. This style of interaction is largely obsolete: most Isabelle proofs are now written using the Isar language and the Proof General interface. However, this paper contains valuable information that is not available elsewhere. Its examples are based on first-order logic rather than higher-order logic.