# HG changeset patch # User Manuel Eberl # Date 1744972381 -7200 # Node ID bb1955def6873407b20d67fc38d6fa0c11ccd2c3 # Parent 904589510439e559a0f3996003b6a70429233c21 added orphaned theory to HOL-Analysis diff -r 904589510439 -r bb1955def687 src/HOL/ROOT --- 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"