| changeset 292 | 293e9c6f22e1 |
| parent 289 | 4e50ff177348 |
| 291:93db7414931d | 292:293e9c6f22e1 |
|---|---|
1 (* Title: thys/UF.thy |
1 (* Title: thys/UF.thy |
2 Author: Jian Xu, Xingyuan Zhang, and Christian Urban |
2 Author: Jian Xu, Xingyuan Zhang, and Christian Urban |
3 Modifications: Sebastiaan Joosten |
|
3 *) |
4 *) |
4 |
5 |
5 chapter {* Construction of a Universal Function *} |
6 chapter {* Construction of a Universal Function *} |
6 |
7 |
7 theory UF |
8 theory UF |