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
     1 (*  Title:      HOL/Complex/ex/ROOT.ML
     2     ID:         $Id$
     3 
     4 Miscellaneous examples involving the Reals, Hyperreals, etc.
     5 *)
     6 
     7 use_thy "BinEx";
     8 no_document (with_path "../../NumberTheory" use_thy) "Factorization";
     9 (*These two examples just need the theory Primes.*)
    10 use_thy "Sqrt";
    11 use_thy "Sqrt_Script";
    12 (*This example also needs the theory Factorization.*)
    13 use_thy "NSPrimes";