| changeset 17042 | da5cfaa258f7 |
| parent 16760 | 5c5f051aaaaa |
| child 17508 | c84af7f39a6b |
| 17041:dee6f7047cae | 17042:da5cfaa258f7 |
|---|---|
12 |
12 |
13 text {* |
13 text {* |
14 Is defined separately to serve as a basis for theory ToyList in the |
14 Is defined separately to serve as a basis for theory ToyList in the |
15 documentation. *} |
15 documentation. *} |
16 |
16 |
17 lemmas wf_induct_rule = wf_induct [rule_format, case_names less, induct set: wf] |
|
18 -- {* belongs to theory @{text Wellfounded_Recursion} *} |
|
19 |
|
20 end |
17 end |