The Isabelle/Isar language has been heavily inspired by the Mizar style, however already from the beginning it has been different in many ways and it has been evolving in different directions than the syntax the Mizar language. These differences were mostly motivated by the particular needs of integration with Isabelle at a particular time, in particular in order to make various proof tactics and other techniques associated with the LCF style available.

In this paper we explore the possibility of emulating the Mizar environment as close as possible inside the Isabelle logical framework. We introduce adaptations to the Isabelle/FOL object logic that correspond to the meta-logic of Mizar, as well as Isar inner syntax notations that correspond to these of the Mizar language. We show how meta-level types can be used to differenciate between the syntactic categories of the Mizar language, such as sets and Mizar types including modes and attributes, and show how they interact with the basic constructs of the Tarski-Groethendieck set theory. We discuss Mizar definitions and provide simple abbreviations that allow the introduction of Mizar predicates, functions, attributes and modes using the Pure definition syntax. We finally consider the definite and indefinite description operators in Mizar and their use to introduce definitions by “means” and “equals”. We demonstrate the usability of the environment on a sample Mizar-style formalization, with cluster inferences and “by” steps performed manually.