author | haftmann |
Fri, 16 Mar 2007 21:32:10 +0100 | |
changeset 22454 | c3654ba76a09 |
parent 21457 | 84a21cf15923 |
child 22844 | 91c05f4b509e |
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 FunDef Extraction begin text {* This is defined separately to serve as a basis for theory ToyList in the documentation. *} end