| changeset 30122 | 1c912a9d8200 |
| parent 29805 | a5da150bd0ab |
| child 30413 | c41afa5607be |
| 30121:5c7bcb296600 | 30122:1c912a9d8200 |
|---|---|
1 (* Title: HOL/ex/ApproximationEx.thy |
1 (* Title: HOL/ex/ApproximationEx.thy |
2 Author: Johannes Hoelzl <hoelzl@in.tum.de> 2009 |
2 Author: Johannes Hoelzl <hoelzl@in.tum.de> 2009 |
3 *) |
3 *) |
4 |
|
4 theory ApproximationEx |
5 theory ApproximationEx |
5 imports "~~/src/HOL/Reflection/Approximation" |
6 imports "~~/src/HOL/Reflection/Approximation" |
6 begin |
7 begin |
7 |
8 |
8 text {* |
9 text {* |