--- a/src/HOL/ex/ROOT.ML Mon May 10 17:37:32 2010 +0200
+++ b/src/HOL/ex/ROOT.ML Mon May 10 11:30:05 2010 -0700
@@ -65,7 +65,8 @@
"Landau",
"Execute_Choice",
"Summation",
- "Gauge_Integration"
+ "Gauge_Integration",
+ "Dedekind_Real"
];
HTML.with_charset "utf-8" (no_document use_thys)