src/HOL/Complex/ex/ROOT.ML

case_tac/induct_tac: use same declarations as cases/induct;

(*  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"
];