author | lcp |
Fri, 16 Dec 1994 17:46:02 +0100 | |
changeset 802 | 2f2fbf0a7e4f |
parent 734 | a3e0fd3c0f2f |
child 1093 | c2b3b7b7a69f |
permissions | -rw-r--r-- |
578
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
1 |
(* Title: ZF/Inductive.ML |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
2 |
ID: $Id$ |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
4 |
Copyright 1993 University of Cambridge |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
5 |
|
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
6 |
(Co)Inductive Definitions for Zermelo-Fraenkel Set Theory |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
7 |
|
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
8 |
Inductive definitions use least fixedpoints with standard products and sums |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
9 |
Coinductive definitions use greatest fixedpoints with Quine products and sums |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
10 |
|
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
11 |
Sums are used only for mutual recursion; |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
12 |
Products are used only to derive "streamlined" induction rules for relations |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
13 |
*) |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
14 |
|
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
15 |
local open Ind_Syntax |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
16 |
in |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
17 |
structure Lfp = |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
18 |
struct |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
19 |
val oper = Const("lfp", [iT,iT-->iT]--->iT) |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
20 |
val bnd_mono = Const("bnd_mono", [iT,iT-->iT]--->oT) |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
21 |
val bnd_monoI = bnd_monoI |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
22 |
val subs = def_lfp_subset |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
23 |
val Tarski = def_lfp_Tarski |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
24 |
val induct = def_induct |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
25 |
end; |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
26 |
|
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
27 |
structure Standard_Prod = |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
28 |
struct |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
29 |
val sigma = Const("Sigma", [iT, iT-->iT]--->iT) |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
30 |
val pair = Const("Pair", [iT,iT]--->iT) |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
31 |
val split_const = Const("split", [[iT,iT]--->iT, iT]--->iT) |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
32 |
val fsplit_const = Const("fsplit", [[iT,iT]--->oT, iT]--->oT) |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
33 |
val pair_iff = Pair_iff |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
34 |
val split_eq = split |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
35 |
val fsplitI = fsplitI |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
36 |
val fsplitD = fsplitD |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
37 |
val fsplitE = fsplitE |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
38 |
end; |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
39 |
|
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
40 |
structure Standard_Sum = |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
41 |
struct |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
42 |
val sum = Const("op +", [iT,iT]--->iT) |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
43 |
val inl = Const("Inl", iT-->iT) |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
44 |
val inr = Const("Inr", iT-->iT) |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
45 |
val elim = Const("case", [iT-->iT, iT-->iT, iT]--->iT) |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
46 |
val case_inl = case_Inl |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
47 |
val case_inr = case_Inr |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
48 |
val inl_iff = Inl_iff |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
49 |
val inr_iff = Inr_iff |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
50 |
val distinct = Inl_Inr_iff |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
51 |
val distinct' = Inr_Inl_iff |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
52 |
end; |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
53 |
end; |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
54 |
|
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
55 |
functor Ind_section_Fun (Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end) |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
56 |
: sig include INTR_ELIM INDRULE end = |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
57 |
struct |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
58 |
structure Intr_elim = |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
59 |
Intr_elim_Fun(structure Inductive=Inductive and Fp=Lfp and |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
60 |
Pr=Standard_Prod and Su=Standard_Sum); |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
61 |
|
734
a3e0fd3c0f2f
ZF INDUCTIVE DEFINITIONS: Simplifying the type checking for mutually
lcp
parents:
578
diff
changeset
|
62 |
structure Indrule = |
a3e0fd3c0f2f
ZF INDUCTIVE DEFINITIONS: Simplifying the type checking for mutually
lcp
parents:
578
diff
changeset
|
63 |
Indrule_Fun (structure Inductive=Inductive and |
a3e0fd3c0f2f
ZF INDUCTIVE DEFINITIONS: Simplifying the type checking for mutually
lcp
parents:
578
diff
changeset
|
64 |
Pr=Standard_Prod and Su=Standard_Sum and Intr_elim=Intr_elim); |
578
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
65 |
|
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
66 |
open Intr_elim Indrule |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
67 |
end; |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
68 |
|
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
69 |
|
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
70 |
structure Ind = Add_inductive_def_Fun |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
71 |
(structure Fp=Lfp and Pr=Standard_Prod and Su=Standard_Sum); |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
72 |
|
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
73 |
|
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
74 |
local open Ind_Syntax |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
75 |
in |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
76 |
structure Gfp = |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
77 |
struct |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
78 |
val oper = Const("gfp", [iT,iT-->iT]--->iT) |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
79 |
val bnd_mono = Const("bnd_mono", [iT,iT-->iT]--->oT) |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
80 |
val bnd_monoI = bnd_monoI |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
81 |
val subs = def_gfp_subset |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
82 |
val Tarski = def_gfp_Tarski |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
83 |
val induct = def_Collect_coinduct |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
84 |
end; |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
85 |
|
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
86 |
structure Quine_Prod = |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
87 |
struct |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
88 |
val sigma = Const("QSigma", [iT, iT-->iT]--->iT) |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
89 |
val pair = Const("QPair", [iT,iT]--->iT) |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
90 |
val split_const = Const("qsplit", [[iT,iT]--->iT, iT]--->iT) |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
91 |
val fsplit_const = Const("qfsplit", [[iT,iT]--->oT, iT]--->oT) |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
92 |
val pair_iff = QPair_iff |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
93 |
val split_eq = qsplit |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
94 |
val fsplitI = qfsplitI |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
95 |
val fsplitD = qfsplitD |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
96 |
val fsplitE = qfsplitE |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
97 |
end; |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
98 |
|
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
99 |
structure Quine_Sum = |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
100 |
struct |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
101 |
val sum = Const("op <+>", [iT,iT]--->iT) |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
102 |
val inl = Const("QInl", iT-->iT) |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
103 |
val inr = Const("QInr", iT-->iT) |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
104 |
val elim = Const("qcase", [iT-->iT, iT-->iT, iT]--->iT) |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
105 |
val case_inl = qcase_QInl |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
106 |
val case_inr = qcase_QInr |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
107 |
val inl_iff = QInl_iff |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
108 |
val inr_iff = QInr_iff |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
109 |
val distinct = QInl_QInr_iff |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
110 |
val distinct' = QInr_QInl_iff |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
111 |
end; |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
112 |
end; |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
113 |
|
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
114 |
|
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
115 |
signature COINDRULE = |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
116 |
sig |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
117 |
val coinduct : thm |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
118 |
end; |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
119 |
|
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
120 |
|
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
121 |
functor CoInd_section_Fun |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
122 |
(Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end) |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
123 |
: sig include INTR_ELIM COINDRULE end = |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
124 |
struct |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
125 |
structure Intr_elim = |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
126 |
Intr_elim_Fun(structure Inductive=Inductive and Fp=Gfp and |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
127 |
Pr=Quine_Prod and Su=Quine_Sum); |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
128 |
|
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
129 |
open Intr_elim |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
130 |
val coinduct = raw_induct |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
131 |
end; |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
132 |
|
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
133 |
|
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
134 |
structure CoInd = |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
135 |
Add_inductive_def_Fun(structure Fp=Gfp and Pr=Quine_Prod and Su=Quine_Sum); |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
136 |
|
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
137 |