equal
deleted
inserted
replaced
1 (* Title: HOL/PreList.thy |
1 (* Title: HOL/PreList.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Tobias Nipkow and Markus Wenzel |
3 Author: Tobias Nipkow and Markus Wenzel |
4 Copyright 2000 TU Muenchen |
4 Copyright 2000 TU Muenchen |
5 |
|
6 A basis for building theory List on. Is defined separately to serve as a |
|
7 basis for theory ToyList in the documentation. |
|
8 *) |
5 *) |
9 |
6 |
10 theory PreList = |
7 header{*A Basis for Building the Theory of Lists*} |
11 Wellfounded_Relations + Presburger + Recdef + Relation_Power: |
|
12 |
8 |
13 (*belongs to theory Divides*) |
9 (*Is defined separately to serve as a basis for theory ToyList in the |
14 declare dvdI [intro?] dvdE [elim?] dvd_trans [trans] |
10 documentation.*) |
15 |
11 |
16 (*belongs to theory Nat*) |
12 theory PreList = Wellfounded_Relations + Presburger + Recdef + Relation_Power: |
17 lemmas less_induct = nat_less_induct [rule_format, case_names less] |
|
18 |
13 |
19 (*belongs to theory Wellfounded_Recursion*) |
14 (*belongs to theory Wellfounded_Recursion*) |
20 lemmas wf_induct_rule = wf_induct [rule_format, case_names less, induct set: wf] |
15 lemmas wf_induct_rule = wf_induct [rule_format, case_names less, induct set: wf] |
21 |
16 |
22 end |
17 end |