equal
deleted
inserted
replaced
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 |
10 imports Wellfounded_Relations Presburger Relation_Power SAT |
|
11 Hilbert_Choice FunDef Extraction |
11 begin |
12 begin |
12 |
13 |
13 text {* |
14 text {* |
14 This is defined separately to serve as a basis for |
15 This is defined separately to serve as a basis for |
15 theory ToyList in the documentation. |
16 theory ToyList in the documentation. |