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 