| author | wenzelm |
| Fri, 17 Nov 2006 02:20:03 +0100 | |
| changeset 21404 | eb85850d3eb7 |
| parent 21330 | 6dd5919e7742 |
| child 21457 | 84a21cf15923 |
| 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 SAT Hilbert_Choice FunDef Extraction begin text {* This is defined separately to serve as a basis for theory ToyList in the documentation. *} end