| changeset 30439 | 57c68b3af2ea |
| parent 30413 | c41afa5607be |
| child 30443 | 873fa77be5f0 |
| 30432:aad3cd70e25a | 30439:57c68b3af2ea |
|---|---|
1 (* Title: HOL/Reflection/Approximation.thy |
1 (* Title: HOL/Decision_Procs/Approximation.thy |
2 Author: Johannes Hoelzl <hoelzl@in.tum.de> 2008 / 2009 |
2 Author: Johannes Hoelzl <hoelzl@in.tum.de> 2008 / 2009 |
3 *) |
3 *) |
4 |
4 |
5 header {* Prove unequations about real numbers by computation *} |
5 header {* Prove unequations about real numbers by computation *} |
6 |
6 |