author | haftmann |
Tue, 19 Sep 2006 15:21:48 +0200 | |
changeset 20591 | 7cbb224598b2 |
parent 17508 | c84af7f39a6b |
child 21256 | 47195501ecf7 |
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 Binomial begin text {* This is defined separately to serve as a basis for theory ToyList in the documentation. *} end