| author | nipkow |
| Sun, 17 Jun 2007 08:56:13 +0200 | |
| changeset 23402 | 6472c689664f |
| parent 22844 | 91c05f4b509e |
| child 23462 | 11728d83794c |
| 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 Recdef Extraction begin text {* This is defined separately to serve as a basis for theory ToyList in the documentation. *} end