| changeset 50530 | 6266e44b3396 |
| parent 49322 | fbb320d02420 |
| child 53107 | 57c7294eac0a |
| 50529:b2aa899b3f2d | 50530:6266e44b3396 |
|---|---|
1 (* Title: Doc/Functions/Fundefs.thy |
1 (* Title: Doc/Functions/Functions.thy |
2 Author: Alexander Krauss, TU Muenchen |
2 Author: Alexander Krauss, TU Muenchen |
3 |
3 |
4 Tutorial for function definitions with the new "function" package. |
4 Tutorial for function definitions with the new "function" package. |
5 *) |
5 *) |
6 |
6 |