| changeset 292 | 293e9c6f22e1 |
| parent 288 | a9003e6d0463 |
| 291:93db7414931d | 292:293e9c6f22e1 |
|---|---|
1 (* Title: thys/Turing_Hoare.thy |
1 (* Title: thys/Turing_Hoare.thy |
2 Author: Jian Xu, Xingyuan Zhang, and Christian Urban |
2 Author: Jian Xu, Xingyuan Zhang, and Christian Urban |
3 Modifications: Sebastiaan Joosten |
|
3 *) |
4 *) |
4 |
5 |
5 chapter {* Hoare Rules for TMs *} |
6 chapter {* Hoare Rules for TMs *} |
6 |
7 |
7 theory Turing_Hoare |
8 theory Turing_Hoare |