equal
deleted
inserted
replaced
7 header{*A Basis for Building the Theory of Lists*} |
7 header{*A Basis for Building the Theory of Lists*} |
8 |
8 |
9 (*Is defined separately to serve as a basis for theory ToyList in the |
9 (*Is defined separately to serve as a basis for theory ToyList in the |
10 documentation.*) |
10 documentation.*) |
11 |
11 |
12 theory PreList = Wellfounded_Relations + Presburger + Recdef + Relation_Power: |
12 theory PreList = |
|
13 Wellfounded_Relations + Presburger + Recdef + Relation_Power + Parity: |
13 |
14 |
14 (*belongs to theory Wellfounded_Recursion*) |
15 (*belongs to theory Wellfounded_Recursion*) |
15 lemmas wf_induct_rule = wf_induct [rule_format, case_names less, induct set: wf] |
16 lemmas wf_induct_rule = wf_induct [rule_format, case_names less, induct set: wf] |
16 |
17 |
17 end |
18 end |