ZFC in HOL
Overview
Introduction
HOL and ProofPower
Membership and Extensionality
Well Foundedness
The Cumulative Hierarchy
The Empty Set and Separation
Pairing and Union
Subset, Powerset and Choice
Replacement
up HOME © RBJ