Abstract
The Cartan fixed point theorems concern the group of holomorphic
automorphisms on a connected open set of Cn. Ciolli et al.
have formalised the one-dimensional case of these theorems in HOL
Light. This entry contains their proofs, ported to Isabelle/HOL. Thus
it addresses the authors' remark that "it would be important to write
a formal proof in a language that can be read by both humans and
machines".