src/HOL/PreList.thy
author krauss
Fri Nov 24 13:44:51 2006 +0100 (2006-11-24)
changeset 21512 3786eb1b69d6
parent 21457 84a21cf15923
child 22844 91c05f4b509e
permissions -rw-r--r--
Lemma "fundef_default_value" uses predicate instead of set.
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@21330
    10
imports Wellfounded_Relations Presburger Relation_Power SAT
haftmann@21457
    11
  FunDef Extraction
nipkow@15131
    12
begin
wenzelm@12397
    13
wenzelm@14577
    14
text {*
haftmann@20591
    15
  This is defined separately to serve as a basis for
haftmann@20591
    16
  theory ToyList in the documentation.
haftmann@20591
    17
*}
wenzelm@14577
    18
wenzelm@8490
    19
end