equal
deleted
inserted
replaced
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 Option + Wellfounded_Relations + NatSimprocs + Recdef + Record + |
12 Relation_Power + Calculation + SVC_Oracle: |
12 Relation_Power + SVC_Oracle: |
|
13 |
|
14 (*belongs to theory Divides*) |
|
15 declare dvd_trans [trans] |
13 |
16 |
14 (*belongs to theory Wellfounded_Recursion*) |
17 (*belongs to theory Wellfounded_Recursion*) |
15 declare wf_induct [induct set: wf] |
18 declare wf_induct [induct set: wf] |
16 |
19 |
17 |
20 |