added orphaned theory to HOL-Analysis
authorManuel Eberl <manuel@pruvisto.org>
Fri, 18 Apr 2025 12:33:01 +0200
changeset 82531 bb1955def687
parent 82530 904589510439
child 82532 b4d4ad6fb9bd
added orphaned theory to HOL-Analysis
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"