nipkow@10519: (*  Title:      HOL/PreList.thy
nipkow@8563:     ID:         $Id$
wenzelm@10733:     Author:     Tobias Nipkow and Markus Wenzel
nipkow@8563:     Copyright   2000 TU Muenchen
nipkow@8563: *)
wenzelm@8490: 
paulson@14125: header{*A Basis for Building the Theory of Lists*}
wenzelm@12020: 
paulson@14125: (*Is defined separately to serve as a basis for theory ToyList in the
paulson@14125: documentation.*)
wenzelm@8490: 
paulson@14125: theory PreList = Wellfounded_Relations + Presburger + Recdef + Relation_Power:
wenzelm@12397: 
wenzelm@10261: (*belongs to theory Wellfounded_Recursion*)
wenzelm@12397: lemmas wf_induct_rule = wf_induct [rule_format, case_names less, induct set: wf]
wenzelm@9066: 
wenzelm@8490: end