more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
header {* Comprehensive Complex Theory *}
theory Complex_Main
imports
Main
Real
SupInf
Complex
Log
Ln
Taylor
Deriv
begin
end