| changeset 66453 | cc19f7ca2ed6 |
| parent 63067 | 0a8a75e400da |
| child 70468 | 8406a2c296e0 |
| 66452:450cefec7c11 | 66453:cc19f7ca2ed6 |
|---|---|
3 *) |
3 *) |
4 |
4 |
5 section \<open>Examples of function definitions\<close> |
5 section \<open>Examples of function definitions\<close> |
6 |
6 |
7 theory Functions |
7 theory Functions |
8 imports Main "~~/src/HOL/Library/Monad_Syntax" |
8 imports Main "HOL-Library.Monad_Syntax" |
9 begin |
9 begin |
10 |
10 |
11 subsection \<open>Very basic\<close> |
11 subsection \<open>Very basic\<close> |
12 |
12 |
13 fun fib :: "nat \<Rightarrow> nat" |
13 fun fib :: "nat \<Rightarrow> nat" |