author | huffman |
Tue, 03 Jul 2007 17:28:36 +0200 | |
changeset 23544 | 4b4165cb3e0d |
parent 23465 | 8f8835aac299 |
child 23708 | b5eb0b4dd17d |
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