src/ZF/Inductive.ML
author clasohm
Tue, 30 Jan 1996 13:42:57 +0100
changeset 1461 6bcb44e4d6e5
parent 1418 f5f97ee67cbb
child 1737 5a4f382455ce
permissions -rw-r--r--
expanded tabs
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
     1
(*  Title:      ZF/Inductive.ML
578
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
     2
    ID:         $Id$
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
578
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
1418
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1093
diff changeset
    15
val iT = Ind_Syntax.iT
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1093
diff changeset
    16
and oT = Ind_Syntax.oT;
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1093
diff changeset
    17
578
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    18
structure Lfp =
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    19
  struct
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
    20
  val oper      = Const("lfp",      [iT,iT-->iT]--->iT)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
    21
  val bnd_mono  = Const("bnd_mono", [iT,iT-->iT]--->oT)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
    22
  val bnd_monoI = bnd_monoI
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
    23
  val subs      = def_lfp_subset
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
    24
  val Tarski    = def_lfp_Tarski
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
    25
  val induct    = def_induct
578
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    26
  end;
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    27
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    28
structure Standard_Prod =
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    29
  struct
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
    30
  val sigma     = Const("Sigma", [iT, iT-->iT]--->iT)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
    31
  val pair      = Const("Pair", [iT,iT]--->iT)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
    32
  val split_const       = Const("split", [[iT,iT]--->iT, iT]--->iT)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
    33
  val fsplit_const      = Const("split", [[iT,iT]--->oT, iT]--->oT)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
    34
  val pair_iff  = Pair_iff
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
    35
  val split_eq  = split
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
    36
  val fsplitI   = splitI
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
    37
  val fsplitD   = splitD
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
    38
  val fsplitE   = splitE
578
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    39
  end;
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    40
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    41
structure Standard_Sum =
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    42
  struct
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
    43
  val sum       = Const("op +", [iT,iT]--->iT)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
    44
  val inl       = Const("Inl", iT-->iT)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
    45
  val inr       = Const("Inr", iT-->iT)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
    46
  val elim      = Const("case", [iT-->iT, iT-->iT, iT]--->iT)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
    47
  val case_inl  = case_Inl
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
    48
  val case_inr  = case_Inr
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
    49
  val inl_iff   = Inl_iff
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
    50
  val inr_iff   = Inr_iff
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
    51
  val distinct  = Inl_Inr_iff
578
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    52
  val distinct' = Inr_Inl_iff
1418
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1093
diff changeset
    53
  val free_SEs  = Ind_Syntax.mk_free_SEs 
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1093
diff changeset
    54
            [distinct, distinct', inl_iff, inr_iff, Standard_Prod.pair_iff]
578
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    55
  end;
1418
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1093
diff changeset
    56
578
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    57
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    58
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
    59
  : sig include INTR_ELIM INDRULE end =
1418
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1093
diff changeset
    60
let
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1093
diff changeset
    61
  structure Intr_elim = 
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1093
diff changeset
    62
      Intr_elim_Fun(structure Inductive=Inductive and Fp=Lfp and 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
    63
                    Pr=Standard_Prod and Su=Standard_Sum);
578
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    64
1418
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1093
diff changeset
    65
  structure Indrule = 
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1093
diff changeset
    66
      Indrule_Fun (structure Inductive=Inductive and 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
    67
                   Pr=Standard_Prod and Su=Standard_Sum and 
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
    68
                       Intr_elim=Intr_elim)
1418
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1093
diff changeset
    69
in 
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1093
diff changeset
    70
   struct 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
    71
   val thy      = Intr_elim.thy
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
    72
   val defs     = Intr_elim.defs
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
    73
   val bnd_mono = Intr_elim.bnd_mono
1418
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1093
diff changeset
    74
   val dom_subset = Intr_elim.dom_subset
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
    75
   val intrs    = Intr_elim.intrs
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
    76
   val elim     = Intr_elim.elim
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
    77
   val mk_cases = Intr_elim.mk_cases
1418
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1093
diff changeset
    78
   open Indrule 
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1093
diff changeset
    79
   end
578
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    80
end;
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    81
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    82
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    83
structure Ind = Add_inductive_def_Fun
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    84
    (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
    85
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    86
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    87
structure Gfp =
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    88
  struct
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
    89
  val oper      = Const("gfp",      [iT,iT-->iT]--->iT)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
    90
  val bnd_mono  = Const("bnd_mono", [iT,iT-->iT]--->oT)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
    91
  val bnd_monoI = bnd_monoI
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
    92
  val subs      = def_gfp_subset
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
    93
  val Tarski    = def_gfp_Tarski
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
    94
  val induct    = def_Collect_coinduct
578
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    95
  end;
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    96
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    97
structure Quine_Prod =
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    98
  struct
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
    99
  val sigma     = Const("QSigma", [iT, iT-->iT]--->iT)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
   100
  val pair      = Const("QPair", [iT,iT]--->iT)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
   101
  val split_const       = Const("qsplit", [[iT,iT]--->iT, iT]--->iT)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
   102
  val fsplit_const      = Const("qsplit", [[iT,iT]--->oT, iT]--->oT)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
   103
  val pair_iff  = QPair_iff
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
   104
  val split_eq  = qsplit
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
   105
  val fsplitI   = qsplitI
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
   106
  val fsplitD   = qsplitD
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
   107
  val fsplitE   = qsplitE
578
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   108
  end;
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   109
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   110
structure Quine_Sum =
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   111
  struct
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
   112
  val sum       = Const("op <+>", [iT,iT]--->iT)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
   113
  val inl       = Const("QInl", iT-->iT)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
   114
  val inr       = Const("QInr", iT-->iT)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
   115
  val elim      = Const("qcase", [iT-->iT, iT-->iT, iT]--->iT)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
   116
  val case_inl  = qcase_QInl
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
   117
  val case_inr  = qcase_QInr
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
   118
  val inl_iff   = QInl_iff
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
   119
  val inr_iff   = QInr_iff
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
   120
  val distinct  = QInl_QInr_iff
578
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   121
  val distinct' = QInr_QInl_iff
1418
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1093
diff changeset
   122
  val free_SEs  = Ind_Syntax.mk_free_SEs 
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1093
diff changeset
   123
            [distinct, distinct', inl_iff, inr_iff, Quine_Prod.pair_iff]
578
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   124
  end;
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   125
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   126
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   127
signature COINDRULE =
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   128
  sig
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   129
  val coinduct : thm
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   130
  end;
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   131
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
functor CoInd_section_Fun
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   134
 (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
   135
    : sig include INTR_ELIM COINDRULE end =
1418
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1093
diff changeset
   136
let
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1093
diff changeset
   137
  structure Intr_elim = 
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1093
diff changeset
   138
      Intr_elim_Fun(structure Inductive=Inductive and Fp=Gfp and 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
   139
                    Pr=Quine_Prod and Su=Quine_Sum);
1418
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1093
diff changeset
   140
in
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1093
diff changeset
   141
   struct
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
   142
   val thy      = Intr_elim.thy
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
   143
   val defs     = Intr_elim.defs
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
   144
   val bnd_mono = Intr_elim.bnd_mono
1418
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1093
diff changeset
   145
   val dom_subset = Intr_elim.dom_subset
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
   146
   val intrs    = Intr_elim.intrs
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
   147
   val elim     = Intr_elim.elim
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
   148
   val mk_cases = Intr_elim.mk_cases
1418
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1093
diff changeset
   149
   val coinduct = Intr_elim.raw_induct
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1093
diff changeset
   150
   end
578
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   151
end;
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   152
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   153
structure CoInd = 
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   154
    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
   155