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