--- a/src/HOL/ROOT Fri Apr 18 12:26:04 2025 +0200 +++ b/src/HOL/ROOT Fri Apr 18 12:33:01 2025 +0200 @@ -108,6 +108,7 @@ "HOL-Real_Asymp" theories Analysis + Finite_Function_Topology (* not part of main file because it imports problematic Sum_any notation *) document_files "root.tex" "root.bib"