src/HOL/Complex/ex/ROOT.ML
author wenzelm
Fri, 10 Aug 2007 15:28:11 +0200
changeset 24216 2e2d81b4f184
parent 23454 c54975167be9
child 24631 c7da302a0346
permissions -rw-r--r--
simultaneous use_thys;

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

if String.isPrefix "smlnj" ml_system then ()  (* FIXME tmp *)
else use_thys ["MIR", "ReflectedFerrack"];