equal
deleted
inserted
replaced
6 A basis for building theory List on. Is defined separately to serve as a |
6 A basis for building theory List on. Is defined separately to serve as a |
7 basis for theory ToyList in the documentation. |
7 basis for theory ToyList in the documentation. |
8 *) |
8 *) |
9 |
9 |
10 theory PreList = |
10 theory PreList = |
11 Wellfounded_Relations + NatSimprocs + Recdef + Relation_Power: |
11 Wellfounded_Relations + Presburger + Recdef + Relation_Power: |
12 |
12 |
13 (*belongs to theory Divides*) |
13 (*belongs to theory Divides*) |
14 declare dvdI [intro?] dvdE [elim?] dvd_trans [trans] |
14 declare dvdI [intro?] dvdE [elim?] dvd_trans [trans] |
15 |
15 |
16 (*belongs to theory Nat*) |
16 (*belongs to theory Nat*) |