src/HOL/PreList.thy
author haftmann
Wed Sep 26 20:27:55 2007 +0200 (2007-09-26)
changeset 24728 e2b3a1065676
parent 24699 c6674504103f
child 24742 73b8b42a36b6
permissions -rw-r--r--
moved Finite_Set before Datatype
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@24632
    10
imports Presburger Relation_Power SAT Recdef Extraction Record 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
paulson@24632
    24
(*Sledgehammer*)
paulson@24632
    25
setup ResAxioms.setup
paulson@24632
    26
wenzelm@8490
    27
end