src/ZF/Inductive.thy
author wenzelm
Wed, 05 Dec 2001 03:07:44 +0100
changeset 12372 cd3a09c7dac9
parent 12208 5efe7b6874fd
child 13259 01fa0c8dbc92
permissions -rw-r--r--
tuned declarations;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
12175
5cf58a1799a7 rearranged inductive package for Isar;
wenzelm
parents: 9491
diff changeset
     1
(*  Title:      ZF/Inductive.thy
5cf58a1799a7 rearranged inductive package for Isar;
wenzelm
parents: 9491
diff changeset
     2
    ID:         $Id$
5cf58a1799a7 rearranged inductive package for Isar;
wenzelm
parents: 9491
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
5cf58a1799a7 rearranged inductive package for Isar;
wenzelm
parents: 9491
diff changeset
     4
    Copyright   1993  University of Cambridge
5cf58a1799a7 rearranged inductive package for Isar;
wenzelm
parents: 9491
diff changeset
     5
5cf58a1799a7 rearranged inductive package for Isar;
wenzelm
parents: 9491
diff changeset
     6
(Co)Inductive Definitions for Zermelo-Fraenkel Set Theory.
5cf58a1799a7 rearranged inductive package for Isar;
wenzelm
parents: 9491
diff changeset
     7
*)
578
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
     8
12175
5cf58a1799a7 rearranged inductive package for Isar;
wenzelm
parents: 9491
diff changeset
     9
theory Inductive = Fixedpt + mono
5cf58a1799a7 rearranged inductive package for Isar;
wenzelm
parents: 9491
diff changeset
    10
  files
12183
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12175
diff changeset
    11
    "ind_syntax.ML"
12175
5cf58a1799a7 rearranged inductive package for Isar;
wenzelm
parents: 9491
diff changeset
    12
    "Tools/cartprod.ML"
5cf58a1799a7 rearranged inductive package for Isar;
wenzelm
parents: 9491
diff changeset
    13
    "Tools/ind_cases.ML"
5cf58a1799a7 rearranged inductive package for Isar;
wenzelm
parents: 9491
diff changeset
    14
    "Tools/inductive_package.ML"
5cf58a1799a7 rearranged inductive package for Isar;
wenzelm
parents: 9491
diff changeset
    15
    "Tools/induct_tacs.ML"
5cf58a1799a7 rearranged inductive package for Isar;
wenzelm
parents: 9491
diff changeset
    16
    "Tools/primrec_package.ML":
5cf58a1799a7 rearranged inductive package for Isar;
wenzelm
parents: 9491
diff changeset
    17
5cf58a1799a7 rearranged inductive package for Isar;
wenzelm
parents: 9491
diff changeset
    18
setup IndCases.setup
12208
5efe7b6874fd setup DatatypeTactics.setup;
wenzelm
parents: 12183
diff changeset
    19
setup DatatypeTactics.setup
2870
6d6fd10a9fdc Now a non-trivial theory so that require_thy can find it
paulson
parents: 805
diff changeset
    20
12372
cd3a09c7dac9 tuned declarations;
wenzelm
parents: 12208
diff changeset
    21
cd3a09c7dac9 tuned declarations;
wenzelm
parents: 12208
diff changeset
    22
(*belongs to theory ZF*)
cd3a09c7dac9 tuned declarations;
wenzelm
parents: 12208
diff changeset
    23
declare bspec [dest?]
cd3a09c7dac9 tuned declarations;
wenzelm
parents: 12208
diff changeset
    24
cd3a09c7dac9 tuned declarations;
wenzelm
parents: 12208
diff changeset
    25
(*belongs to theory upair*)
cd3a09c7dac9 tuned declarations;
wenzelm
parents: 12208
diff changeset
    26
declare UnI1 [elim?]  UnI2 [elim?]
cd3a09c7dac9 tuned declarations;
wenzelm
parents: 12208
diff changeset
    27
2870
6d6fd10a9fdc Now a non-trivial theory so that require_thy can find it
paulson
parents: 805
diff changeset
    28
end