src/HOL/PreList.thy
author wenzelm
Thu, 22 Dec 2005 00:28:36 +0100
changeset 18457 356a9f711899
parent 17508 c84af7f39a6b
child 20591 7cbb224598b2
permissions -rw-r--r--
structure ProjectRule; updated auxiliary facts for induct method; tuned proofs;
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
14125
paulson
parents: 13878
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
17508
c84af7f39a6b tuned theory dependencies;
wenzelm
parents: 17042
diff changeset
    10
imports Wellfounded_Relations Presburger Relation_Power Binomial
15131
c69542757a4d New theory header syntax.
nipkow
parents: 14577
diff changeset
    11
begin
12397
6766aa05e4eb less_induct, wf_induct_rule;
wenzelm
parents: 12304
diff changeset
    12
14577
dbb95b825244 tuned document;
wenzelm
parents: 14430
diff changeset
    13
text {*
dbb95b825244 tuned document;
wenzelm
parents: 14430
diff changeset
    14
  Is defined separately to serve as a basis for theory ToyList in the
dbb95b825244 tuned document;
wenzelm
parents: 14430
diff changeset
    15
  documentation. *}
dbb95b825244 tuned document;
wenzelm
parents: 14430
diff changeset
    16
8490
6e0f23304061 added HOL/PreLIst.thy;
wenzelm
parents:
diff changeset
    17
end