| changeset 41413 | 64cd30d6b0b8 |
| parent 40169 | 11ea439d947f |
| child 41817 | c7be23634728 |
| 41412:35f30e07fe0d | 41413:64cd30d6b0b8 |
|---|---|
3 *) |
3 *) |
4 |
4 |
5 header {* Examples of function definitions *} |
5 header {* Examples of function definitions *} |
6 |
6 |
7 theory Fundefs |
7 theory Fundefs |
8 imports Parity Monad_Syntax |
8 imports Parity "~~/src/HOL/Library/Monad_Syntax" |
9 begin |
9 begin |
10 |
10 |
11 subsection {* Very basic *} |
11 subsection {* Very basic *} |
12 |
12 |
13 fun fib :: "nat \<Rightarrow> nat" |
13 fun fib :: "nat \<Rightarrow> nat" |