src/HOL/PreList.thy
author urbanc
Tue Jun 05 09:56:19 2007 +0200 (2007-06-05)
changeset 23243 a37d3e6e8323
parent 22844 91c05f4b509e
child 23462 11728d83794c
permissions -rw-r--r--
included Class.thy in the compiling process for Nominal/Examples
     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 Wellfounded_Relations Presburger Relation_Power SAT
    11   FunDef Recdef Extraction
    12 begin
    13 
    14 text {*
    15   This is defined separately to serve as a basis for
    16   theory ToyList in the documentation.
    17 *}
    18 
    19 end