src/HOL/Real/ex/ROOT.ML

activate dead code, make document work;

(*  Title:      HOL/Real/ex/ROOT.ML
    ID:         $Id$

Miscellaneous HOL-Real Examples.
*)

no_document use_thy "Primes";
time_use_thy "Sqrt";
time_use_thy "Sqrt_Script";
time_use_thy "BinEx";