| author | krauss |
| Tue, 08 Apr 2008 20:14:36 +0200 | |
| changeset 26583 | 9f81ab1b7b64 |
| parent 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 Record Presburger SAT Recdef Extraction Relation_Power begin text {* This is defined separately to serve as a basis for theory ToyList in the documentation. *} end