author | haftmann |
Wed, 02 Jan 2008 15:14:20 +0100 | |
changeset 25765 | 49580bd58a21 |
parent 24631 | c7da302a0346 |
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 |
||
24216 | 4 |
Miscellaneous examples. |
13957 | 5 |
*) |
6 |
||
24216 | 7 |
no_document use_thys [ |
8 |
"../../NumberTheory/Factorization", |
|
9 |
"BigO", |
|
10 |
"NatPair" |
|
11 |
]; |
|
17198 | 12 |
|
24216 | 13 |
use_thys [ |
14 |
"BinEx", |
|
15 |
"Sqrt", |
|
16 |
"Sqrt_Script", |
|
17 |
"NSPrimes", |
|
18 |
"BigO_Complex", |
|
19106
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
17198
diff
changeset
|
19 |
|
24216 | 20 |
"Arithmetic_Series_Complex", |
21 |
"HarmonicSeries", |
|
19109 | 22 |
|
24631 | 23 |
"DenumRat", |
24 |
||
25 |
"MIR", |
|
26 |
"ReflectedFerrack" |
|
24216 | 27 |
]; |
19640
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
19469
diff
changeset
|
28 |