All files are translated from the corresponding code files of Harrision in HOL-Light. They were developed in HOL4 (Kananaskis 6). See [1] for the documentation.
Ported to HOL4 (Kananaskis 14) by Chun Tian.
[1] Z. Shi, Y. Guan, X. Li, Formalization of Complex Analysis and Matrix Theory, Springer, Singapore, 2020. doi:10.1007/978-981-15-7261-6.