| changeset 58886 | 8a6cac7c7247 |
| parent 58860 | fee7cfa69c50 |
| child 59807 | 22bc39064290 |
| 58885:47fdd4f40d00 | 58886:8a6cac7c7247 |
|---|---|
1 (* Title: HOL/MicroJava/DFA/Listn.thy |
1 (* Title: HOL/MicroJava/DFA/Listn.thy |
2 Author: Tobias Nipkow |
2 Author: Tobias Nipkow |
3 Copyright 2000 TUM |
3 Copyright 2000 TUM |
4 *) |
4 *) |
5 |
5 |
6 header {* \isaheader{Fixed Length Lists} *} |
6 section {* Fixed Length Lists *} |
7 |
7 |
8 theory Listn |
8 theory Listn |
9 imports Err |
9 imports Err |
10 begin |
10 begin |
11 |
11 |