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: 
haftmann@20591: header {* A Basis for Building the Theory of Lists *}
wenzelm@12020: 
nipkow@15131: theory PreList
haftmann@23708: imports Presburger Relation_Power SAT Recdef Extraction Record
nipkow@15131: begin
wenzelm@12397: 
wenzelm@14577: text {*
haftmann@20591:   This is defined separately to serve as a basis for
haftmann@20591:   theory ToyList in the documentation.
haftmann@20591: *}
wenzelm@14577: 
wenzelm@8490: end
haftmann@23708: