src/HOL/Complex/ex/ROOT.ML
author paulson
Thu Jul 01 12:29:53 2004 +0200 (2004-07-01)
changeset 15013 34264f5e4691
parent 13966 2160abf7cfe7
child 17198 ffe8efe856e3
permissions -rw-r--r--
new treatment of binary numerals
paulson@13966
     1
(*  Title:      HOL/Complex/ex/ROOT.ML
paulson@13957
     2
    ID:         $Id$
paulson@13957
     3
paulson@13966
     4
Miscellaneous examples involving the Reals, Hyperreals, etc.
paulson@13957
     5
*)
paulson@13957
     6
paulson@13966
     7
use_thy "BinEx";
paulson@13957
     8
no_document (with_path "../../NumberTheory" use_thy) "Factorization";
paulson@13957
     9
(*These two examples just need the theory Primes.*)
paulson@13957
    10
use_thy "Sqrt";
paulson@13957
    11
use_thy "Sqrt_Script";
paulson@13957
    12
(*This example also needs the theory Factorization.*)
paulson@13957
    13
use_thy "NSPrimes";