changeset 58889 | 5b7a9633cfa8 |
parent 45010 | 8a4db903039f |
child 58971 | 8c9a319821b3 |
58888:9537bf1c4853 | 58889:5b7a9633cfa8 |
---|---|
1 (* Title: CCL/ex/List.thy |
1 (* Title: CCL/ex/List.thy |
2 Author: Martin Coen, Cambridge University Computer Laboratory |
2 Author: Martin Coen, Cambridge University Computer Laboratory |
3 Copyright 1993 University of Cambridge |
3 Copyright 1993 University of Cambridge |
4 *) |
4 *) |
5 |
5 |
6 header {* Programs defined over lists *} |
6 section {* Programs defined over lists *} |
7 |
7 |
8 theory List |
8 theory List |
9 imports Nat |
9 imports Nat |
10 begin |
10 begin |
11 |
11 |