author | haftmann |
Fri, 07 Dec 2007 15:07:59 +0100 | |
changeset 25571 | c9e39eafc7a0 |
parent 25517 | 36d710d1dbce |
child 25591 | 0792e02973cc |
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 ATP_Linkup begin text {* This is defined separately to serve as a basis for theory ToyList in the documentation. *} end