author | haftmann |
Thu, 04 Oct 2007 19:41:55 +0200 | |
changeset 24841 | df8448bc7a8b |
parent 23454 | c54975167be9 |
child 27964 | 1e0303048c0b |
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 |
23454
c54975167be9
replaced Real/Ferrante-Rackoff tool by generic version in Main HOL;
wenzelm
parents:
20505
diff
changeset
|
5 |
imports ContNotDenum RealVector |
15536 | 6 |
begin |
19640
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
19023
diff
changeset
|
7 |
end |