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 Barith Recdef Relation_Power Parity |
10 imports Wellfounded_Relations Presburger Recdef Relation_Power Parity |
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 Is defined separately to serve as a basis for theory ToyList in the |
15 documentation. *} |
15 documentation. *} |