author  wenzelm 
Sun, 10 Jun 2007 21:06:59 +0200  
changeset 23301  4c7e6d295980 
parent 23264  324622260d29 
child 23454  c54975167be9 
permissions  rwrr 
13966
2160abf7cfe7
removal of the image HOLReal and merging of HOLRealex with HOLComplexex
paulson
parents:
13957
diff
changeset

1 
(* Title: HOL/Complex/ex/ROOT.ML 
13957  2 
ID: $Id$ 
3 

13966
2160abf7cfe7
removal of the image HOLReal and merging of HOLRealex with HOLComplexex
paulson
parents:
13957
diff
changeset

4 
Miscellaneous examples involving the Reals, Hyperreals, etc. 
13957  5 
*) 
6 

13966
2160abf7cfe7
removal of the image HOLReal and merging of HOLRealex with HOLComplexex
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"; 
19640
40ec89317425
added Ferrante and Rackoff Algorithm  by Amine Chaieb;
wenzelm
parents:
19469
diff
changeset

23 

40ec89317425
added Ferrante and Rackoff Algorithm  by Amine Chaieb;
wenzelm
parents:
19469
diff
changeset

24 
use_thy "Ferrante_Rackoff_Ex"; 
23301
4c7e6d295980
disabled theories MIR and ReflectedFerrack for smlnj (temporarily);
wenzelm
parents:
23264
diff
changeset

25 

4c7e6d295980
disabled theories MIR and ReflectedFerrack for smlnj (temporarily);
wenzelm
parents:
23264
diff
changeset

26 
if String.isPrefix "smlnj" ml_system then () (* FIXME tmp *) 
4c7e6d295980
disabled theories MIR and ReflectedFerrack for smlnj (temporarily);
wenzelm
parents:
23264
diff
changeset

27 
else use_thy "MIR"; 
4c7e6d295980
disabled theories MIR and ReflectedFerrack for smlnj (temporarily);
wenzelm
parents:
23264
diff
changeset

28 

4c7e6d295980
disabled theories MIR and ReflectedFerrack for smlnj (temporarily);
wenzelm
parents:
23264
diff
changeset

29 
if String.isPrefix "smlnj" ml_system then () (* FIXME tmp *) 
4c7e6d295980
disabled theories MIR and ReflectedFerrack for smlnj (temporarily);
wenzelm
parents:
23264
diff
changeset

30 
else use_thy "ReflectedFerrack"; 