| changeset 292 | 293e9c6f22e1 |
| parent 291 | 93db7414931d |
| 291:93db7414931d | 292:293e9c6f22e1 |
|---|---|
1 (* Title: thys/Recursive.thy |
|
2 Author: Jian Xu, Xingyuan Zhang, and Christian Urban |
|
3 Modifications: Sebastiaan Joosten |
|
4 *) |
|
5 |
|
1 theory Recursive |
6 theory Recursive |
2 imports Abacus Rec_Def Abacus_Hoare |
7 imports Abacus Rec_Def Abacus_Hoare |
3 begin |
8 begin |
4 |
9 |
5 fun addition :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> abc_prog" |
10 fun addition :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> abc_prog" |