src/HOL/PreList.thy
author wenzelm
Thu Oct 04 20:29:42 2007 +0200 (2007-10-04)
changeset 24850 0cfd722ab579
parent 24742 73b8b42a36b6
child 25517 36d710d1dbce
permissions -rw-r--r--
Name.uu, Name.aT;
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
paulson@24742
    10
imports ATP_Linkup
nipkow@24616
    11
uses "Tools/function_package/lexicographic_order.ML"
nipkow@24616
    12
     "Tools/function_package/fundef_datatype.ML"
nipkow@15131
    13
begin
wenzelm@12397
    14
wenzelm@14577
    15
text {*
haftmann@20591
    16
  This is defined separately to serve as a basis for
haftmann@20591
    17
  theory ToyList in the documentation.
haftmann@20591
    18
*}
wenzelm@14577
    19
nipkow@24616
    20
(* The lexicographic_order method and the "fun" command *)
nipkow@24616
    21
setup LexicographicOrder.setup
nipkow@24616
    22
setup FundefDatatype.setup
nipkow@24616
    23
wenzelm@8490
    24
end