| author | aspinall | 
| Thu, 15 Sep 2005 16:15:22 +0200 | |
| changeset 17407 | 38e0219ec022 | 
| parent 17042 | da5cfaa258f7 | 
| child 17508 | c84af7f39a6b | 
| permissions | -rw-r--r-- | 
(* Title: HOL/PreList.thy ID: $Id$ Author: Tobias Nipkow and Markus Wenzel Copyright 2000 TU Muenchen *) header{*A Basis for Building the Theory of Lists*} theory PreList imports Wellfounded_Relations Presburger Relation_Power GCD begin text {* Is defined separately to serve as a basis for theory ToyList in the documentation. *} end