## A Comparison of HOL-ST and Isabelle/ZF

*Sten Agerholm*, University of Cambridge Computer Laboratory.

The use of higher order logic (simple type theory) is often limited by
its restrictive type system. Set theory allows many constructions on
sets that are not possible on types in higher order logic. This paper
presents a comparison of two theorem provers supporting set theory,
namely HOL-ST and Isabelle/ZF, based on a formalization of the inverse
limit construction of domain theory; this construction cannot be
formalized in higher order logic directly. We argue that whilst the
combination of higher order logic and set theory in HOL-ST has
advantages over the first order set theory in Isabelle/ZF, the proof
infrastructure of Isabelle/ZF has better support for set theory proofs
than HOL-ST. Proofs in Isabelle/ZF are both considerably shorter and
easier to write.