equal
deleted
inserted
replaced
10 theory PreList = |
10 theory PreList = |
11 Option + Wellfounded_Relations + NatSimprocs + Recdef + Record + |
11 Option + Wellfounded_Relations + NatSimprocs + Recdef + Record + |
12 Relation_Power + SVC_Oracle: |
12 Relation_Power + SVC_Oracle: |
13 |
13 |
14 (*belongs to theory Divides*) |
14 (*belongs to theory Divides*) |
15 declare dvd_trans [trans] |
15 declare dvdI [intro?] dvdE [elim?] dvd_trans [trans] |
16 |
16 |
17 (*belongs to theory Wellfounded_Recursion*) |
17 (*belongs to theory Wellfounded_Recursion*) |
18 declare wf_induct [induct set: wf] |
18 declare wf_induct [induct set: wf] |
19 |
19 |
20 |
20 |