author | huffman |
Tue, 12 Sep 2006 07:49:07 +0200 | |
changeset 20505 | 1e223f64bd59 |
parent 19640 | 40ec89317425 |
child 23454 | c54975167be9 |
permissions | -rw-r--r-- |
19640
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
19023
diff
changeset
|
1 |
|
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
19023
diff
changeset
|
2 |
(* $Id$ *) |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
19023
diff
changeset
|
3 |
|
15536 | 4 |
theory Real |
20505 | 5 |
imports ContNotDenum Ferrante_Rackoff RealVector |
15536 | 6 |
begin |
19640
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
19023
diff
changeset
|
7 |
end |