src/HOL/PreList.thy
author haftmann
Tue Jul 10 17:30:49 2007 +0200 (2007-07-10)
changeset 23708 b5eb0b4dd17d
parent 23465 8f8835aac299
child 24616 fac3dd4ade83
permissions -rw-r--r--
clarified import
nipkow@10519
     1
(*  Title:      HOL/PreList.thy
nipkow@8563
     2
    ID:         $Id$
wenzelm@10733
     3
    Author:     Tobias Nipkow and Markus Wenzel
nipkow@8563
     4
    Copyright   2000 TU Muenchen
nipkow@8563
     5
*)
wenzelm@8490
     6
haftmann@20591
     7
header {* A Basis for Building the Theory of Lists *}
wenzelm@12020
     8
nipkow@15131
     9
theory PreList
haftmann@23708
    10
imports Presburger Relation_Power SAT Recdef Extraction Record
nipkow@15131
    11
begin
wenzelm@12397
    12
wenzelm@14577
    13
text {*
haftmann@20591
    14
  This is defined separately to serve as a basis for
haftmann@20591
    15
  theory ToyList in the documentation.
haftmann@20591
    16
*}
wenzelm@14577
    17
wenzelm@8490
    18
end
haftmann@23708
    19