src/HOL/PreList.thy
author haftmann
Mon Aug 14 13:46:06 2006 +0200 (2006-08-14)
changeset 20380 14f9f2a1caa6
parent 17508 c84af7f39a6b
child 20591 7cbb224598b2
permissions -rw-r--r--
simplified code generator setup
     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 Binomial
    11 begin
    12 
    13 text {*
    14   Is defined separately to serve as a basis for theory ToyList in the
    15   documentation. *}
    16 
    17 end