src/HOL/Complex/ex/ROOT.ML

more markup for inner and outer syntax;
added enclose;

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

Miscellaneous examples involving the Reals, Hyperreals, etc.
*)

use_thy "BinEx";
no_document (with_path "../../NumberTheory" use_thy) "Factorization";
(*These two examples just need the theory Primes.*)
use_thy "Sqrt";
use_thy "Sqrt_Script";
(*This example also needs the theory Factorization.*)
use_thy "NSPrimes";

no_document use_thy "BigO";
use_thy "BigO_Complex";

use_thy "Arithmetic_Series_Complex";
use_thy "HarmonicSeries";

no_document use_thy "NatPair";
use_thy "DenumRat";

if String.isPrefix "smlnj" ml_system then ()  (* FIXME tmp *)
else use_thy "MIR";

if String.isPrefix "smlnj" ml_system then ()  (* FIXME tmp *)
else use_thy "ReflectedFerrack";