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 Option + Wellfounded_Relations + NatSimprocs + Recdef + Record + |
11 Wellfounded_Relations + NatSimprocs + Recdef + Relation_Power: |
12 Relation_Power: |
|
13 |
12 |
14 (*belongs to theory Divides*) |
13 (*belongs to theory Divides*) |
15 declare dvdI [intro?] dvdE [elim?] dvd_trans [trans] |
14 declare dvdI [intro?] dvdE [elim?] dvd_trans [trans] |
16 |
15 |
17 (*belongs to theory Nat*) |
16 (*belongs to theory Nat*) |