This paper presents the first version of a Typol interactive, tactic-driven, theorem prover called Theo. Theorem prover means here proof development system. Typol is the programming language that implements Natural Semantics -a semantics pioneered by G. Plotkin under the name Structural Operational Semantics- in the Centaur meta-compiler. Centaur provides a pleasant graphic man-machine interface that Theo can use, for the user's advantage. Both the meta and the object levels of our theorem prover are logics presented in Typol. In other words, Theo is written in Typol and proves theorems of an object logic also written in Typol. Other important features of Theo are the form chosen for representing proofs, and the way proofs are performed. The internal form of the proofs is a very compact form, expressed with combinators, that is closely related to the lambda-calculus used in Automath and its descendants. Meanwhile, Theo performs proofs by a pure calculus on proofs, using a resolution rule. Proofs may be incomplete, and may contain variables. The paper presents an implementation of the Calculus of Constructions of Thierry Coquand and Gérard Huet, as an example of an object logic for Theo. It also presents the -very few- tactics that have been implemented so far. Our representation of proofs is discussed and compared with other existing forms. Differences with other existing systems are discussed at length.