author | kleing |
Wed, 26 Apr 2006 07:01:33 +0200 | |
changeset 19469 | 958d2f2dd8d4 |
parent 19358 | 9cd12369e753 |
child 19640 | 40ec89317425 |
permissions | -rw-r--r-- |
13966
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
13957
diff
changeset
|
1 |
(* Title: HOL/Complex/ex/ROOT.ML |
13957 | 2 |
ID: $Id$ |
3 |
||
13966
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
13957
diff
changeset
|
4 |
Miscellaneous examples involving the Reals, Hyperreals, etc. |
13957 | 5 |
*) |
6 |
||
13966
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
13957
diff
changeset
|
7 |
use_thy "BinEx"; |
13957 | 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"; |
|
17198 | 14 |
|
15 |
no_document use_thy "BigO"; |
|
16 |
use_thy "BigO_Complex"; |
|
19106
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
17198
diff
changeset
|
17 |
|
19358 | 18 |
use_thy "Arithmetic_Series_Complex"; |
19106
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
17198
diff
changeset
|
19 |
use_thy "HarmonicSeries"; |
19109 | 20 |
|
21 |
no_document use_thy "NatPair"; |
|
19108
6f8c1343341b
* denumerability of rationals by Benjamin Porter, based on NatPair (by Stefan Richter)
kleing
parents:
19106
diff
changeset
|
22 |
use_thy "DenumRat"; |