equal
deleted
inserted
replaced
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 Wellfounded_Relations + Presburger + Recdef + Relation_Power + Parity: |
10 import Wellfounded_Relations Presburger Recdef Relation_Power Parity |
|
11 begin |
11 |
12 |
12 text {* |
13 text {* |
13 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 |
14 documentation. *} |
15 documentation. *} |
15 |
16 |