1.1 --- a/src/HOL/ex/ROOT.ML	Wed Nov 03 12:20:33 2010 +0100
     1.2 +++ b/src/HOL/ex/ROOT.ML	Wed Nov 03 12:20:33 2010 +0100
     1.3 @@ -66,7 +66,8 @@
     1.4    "Execute_Choice",
     1.5    "Summation",
     1.6    "Gauge_Integration",
     1.7 -  "Dedekind_Real"
     1.8 +  "Dedekind_Real",
     1.9 +  "Quicksort"
    1.10  ];
    1.11  
    1.12  HTML.with_charset "utf-8" (no_document use_thys)