src/HOL/Complex/ex/ROOT.ML
changeset 19106 6e6b5b1fdc06
parent 17198 ffe8efe856e3
child 19108 6f8c1343341b
--- a/src/HOL/Complex/ex/ROOT.ML	Sun Feb 19 02:11:27 2006 +0100
+++ b/src/HOL/Complex/ex/ROOT.ML	Sun Feb 19 13:21:32 2006 +0100
@@ -14,3 +14,6 @@
 
 no_document use_thy "BigO";
 use_thy "BigO_Complex";
+
+use_thy "ASeries_Complex";
+use_thy "HarmonicSeries";