[isabelle] New AFP article: The Cartan Fixed Point Theorems



The Cartan Fixed Point Theorems
Lawrence Paulson

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".

http://afp.sourceforge.net/entries/Cartan_FP.shtml

Enjoy!

Attachment: smime.p7s
Description: S/MIME Cryptographic Signature



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.