This formalizes many theorems of inner model theory (IMT), starting from basic properties of L (but using the J-hierarchy throughout) up to models with Woodin cardinals.

Bibliography:

• Jen71 = Ronald Jensen, The Fine Structure of the Constructible Hierarchy