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