src/HOL/PreList.thy
author wenzelm
Fri Mar 28 19:43:54 2008 +0100 (2008-03-28)
changeset 26462 dac4e2bce00d
parent 25591 0792e02973cc
permissions -rw-r--r--
avoid rebinding of existing facts;
     1 (*  Title:      HOL/PreList.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow and Markus Wenzel
     4     Copyright   2000 TU Muenchen
     5 *)
     6 
     7 header {* A Basis for Building the Theory of Lists *}
     8 
     9 theory PreList
    10 imports Record Presburger SAT Recdef Extraction Relation_Power
    11 begin
    12 
    13 text {*
    14   This is defined separately to serve as a basis for
    15   theory ToyList in the documentation.
    16 *}
    17 
    18 end