src/HOL/PreList.thy
author haftmann
Wed, 22 Nov 2006 10:20:17 +0100
changeset 21457 84a21cf15923
parent 21330 6dd5919e7742
child 22844 91c05f4b509e
permissions -rw-r--r--
does not import Hilber_Choice any longer
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
10519
ade64af4c57c hide many names from Datatype_Universe.
nipkow
parents: 10261
diff changeset
     1
(*  Title:      HOL/PreList.thy
8563
2746bc9a7ef2 comments
nipkow
parents: 8490
diff changeset
     2
    ID:         $Id$
10733
59f82484e000 hide type node item;
wenzelm
parents: 10680
diff changeset
     3
    Author:     Tobias Nipkow and Markus Wenzel
8563
2746bc9a7ef2 comments
nipkow
parents: 8490
diff changeset
     4
    Copyright   2000 TU Muenchen
2746bc9a7ef2 comments
nipkow
parents: 8490
diff changeset
     5
*)
8490
6e0f23304061 added HOL/PreLIst.thy;
wenzelm
parents:
diff changeset
     6
20591
7cbb224598b2 text cleanup
haftmann
parents: 17508
diff changeset
     7
header {* A Basis for Building the Theory of Lists *}
12020
a24373086908 theory Calculation move to Set;
wenzelm
parents: 11955
diff changeset
     8
15131
c69542757a4d New theory header syntax.
nipkow
parents: 14577
diff changeset
     9
theory PreList
21330
6dd5919e7742 PreList = Main - List
haftmann
parents: 21256
diff changeset
    10
imports Wellfounded_Relations Presburger Relation_Power SAT
21457
84a21cf15923 does not import Hilber_Choice any longer
haftmann
parents: 21330
diff changeset
    11
  FunDef Extraction
15131
c69542757a4d New theory header syntax.
nipkow
parents: 14577
diff changeset
    12
begin
12397
6766aa05e4eb less_induct, wf_induct_rule;
wenzelm
parents: 12304
diff changeset
    13
14577
dbb95b825244 tuned document;
wenzelm
parents: 14430
diff changeset
    14
text {*
20591
7cbb224598b2 text cleanup
haftmann
parents: 17508
diff changeset
    15
  This is defined separately to serve as a basis for
7cbb224598b2 text cleanup
haftmann
parents: 17508
diff changeset
    16
  theory ToyList in the documentation.
7cbb224598b2 text cleanup
haftmann
parents: 17508
diff changeset
    17
*}
14577
dbb95b825244 tuned document;
wenzelm
parents: 14430
diff changeset
    18
8490
6e0f23304061 added HOL/PreLIst.thy;
wenzelm
parents:
diff changeset
    19
end