equal
deleted
inserted
replaced
12 Relation_Power + SVC_Oracle: |
12 Relation_Power + SVC_Oracle: |
13 |
13 |
14 (*belongs to theory Divides*) |
14 (*belongs to theory Divides*) |
15 declare dvdI [intro?] dvdE [elim?] dvd_trans [trans] |
15 declare dvdI [intro?] dvdE [elim?] dvd_trans [trans] |
16 |
16 |
|
17 (*belongs to theory Nat*) |
|
18 lemmas less_induct = nat_less_induct [rule_format, case_names less] |
|
19 |
17 (*belongs to theory Wellfounded_Recursion*) |
20 (*belongs to theory Wellfounded_Recursion*) |
18 declare wf_induct [induct set: wf] |
21 lemmas wf_induct_rule = wf_induct [rule_format, case_names less, induct set: wf] |
19 |
22 |
20 |
23 |
21 (* generic summation indexed over nat *) |
24 (* generic summation indexed over nat *) |
22 |
25 |
23 consts |
26 consts |