changeset 13957 | 10dbf16be15f |
child 13966 | 2160abf7cfe7 |
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Complex/ex/ROOT.ML Mon May 05 18:22:31 2003 +0200 @@ -0,0 +1,12 @@ +(* Title: HOL/Hyperreal/ex/ROOT.ML + ID: $Id$ + +Miscellaneous HOL-Hyperreal Examples. +*) + +no_document (with_path "../../NumberTheory" use_thy) "Factorization"; +(*These two examples just need the theory Primes.*) +use_thy "Sqrt"; +use_thy "Sqrt_Script"; +(*This example also needs the theory Factorization.*) +use_thy "NSPrimes";