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