equal
deleted
inserted
replaced
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Tobias Nipkow and Markus Wenzel |
3 Author: Tobias Nipkow and Markus Wenzel |
4 Copyright 2000 TU Muenchen |
4 Copyright 2000 TU Muenchen |
5 *) |
5 *) |
6 |
6 |
7 header{*A Basis for Building the Theory of Lists*} |
7 header {* A Basis for Building the Theory of Lists *} |
8 |
8 |
9 theory PreList |
9 theory PreList |
10 imports Wellfounded_Relations Presburger Relation_Power Binomial |
10 imports Wellfounded_Relations Presburger Relation_Power Binomial |
11 begin |
11 begin |
12 |
12 |
13 text {* |
13 text {* |
14 Is defined separately to serve as a basis for theory ToyList in the |
14 This is defined separately to serve as a basis for |
15 documentation. *} |
15 theory ToyList in the documentation. |
|
16 *} |
16 |
17 |
17 end |
18 end |