| author | wenzelm |
| Wed, 25 Jul 2007 22:20:50 +0200 | |
| changeset 23988 | aa46577f4f44 |
| parent 23708 | b5eb0b4dd17d |
| child 24616 | fac3dd4ade83 |
| 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 Presburger Relation_Power SAT Recdef Extraction Record begin text {* This is defined separately to serve as a basis for theory ToyList in the documentation. *} end