src/HOL/Complex/ex/ROOT.ML

commands 'use' and 'ML' now thy_decl;
removed obsolete 'ML_setup' -- superceded by 'ML';

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

Miscellaneous examples.
*)

no_document use_thys [
  "../../NumberTheory/Factorization",
  "BigO",
  "NatPair"
];

use_thys [
  "BinEx",
  "Sqrt",
  "Sqrt_Script",
  "NSPrimes",
  "BigO_Complex",

  "Arithmetic_Series_Complex",
  "HarmonicSeries",

  "DenumRat",
  
  "MIR",
  "ReflectedFerrack"
];