| author | nipkow |
| Tue, 04 Oct 2005 23:30:46 +0200 | |
| changeset 17761 | 2c42d0a94f58 |
| parent 17508 | c84af7f39a6b |
| child 20591 | 7cbb224598b2 |
| 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 {* Is defined separately to serve as a basis for theory ToyList in the documentation. *} end