src/ZF/Inductive.ML
changeset 6093 87bf8c03b169
parent 6053 8a1059aa01f0
child 10216 e928bdf62014
     1.1 --- a/src/ZF/Inductive.ML	Tue Jan 12 13:54:51 1999 +0100
     1.2 +++ b/src/ZF/Inductive.ML	Tue Jan 12 15:17:37 1999 +0100
     1.3 @@ -17,8 +17,8 @@
     1.4  
     1.5  structure Lfp =
     1.6    struct
     1.7 -  val oper      = Const("lfp",      [iT,iT-->iT]--->iT)
     1.8 -  val bnd_mono  = Const("bnd_mono", [iT,iT-->iT]--->oT)
     1.9 +  val oper      = Const("Fixedpt.lfp", [iT,iT-->iT]--->iT)
    1.10 +  val bnd_mono  = Const("Fixedpt.bnd_mono", [iT,iT-->iT]--->oT)
    1.11    val bnd_monoI = bnd_monoI
    1.12    val subs      = def_lfp_subset
    1.13    val Tarski    = def_lfp_Tarski
    1.14 @@ -64,8 +64,8 @@
    1.15  
    1.16  structure Gfp =
    1.17    struct
    1.18 -  val oper      = Const("gfp",      [iT,iT-->iT]--->iT)
    1.19 -  val bnd_mono  = Const("bnd_mono", [iT,iT-->iT]--->oT)
    1.20 +  val oper      = Const("Fixedpt.gfp", [iT,iT-->iT]--->iT)
    1.21 +  val bnd_mono  = Const("Fixedpt.bnd_mono", [iT,iT-->iT]--->oT)
    1.22    val bnd_monoI = bnd_monoI
    1.23    val subs      = def_gfp_subset
    1.24    val Tarski    = def_gfp_Tarski
    1.25 @@ -74,9 +74,9 @@
    1.26  
    1.27  structure Quine_Prod =
    1.28    struct
    1.29 -  val sigma     = Const("QSigma", [iT, iT-->iT]--->iT)
    1.30 -  val pair      = Const("QPair", [iT,iT]--->iT)
    1.31 -  val split_name = "qsplit"
    1.32 +  val sigma     = Const("QPair.QSigma", [iT, iT-->iT]--->iT)
    1.33 +  val pair      = Const("QPair.QPair", [iT,iT]--->iT)
    1.34 +  val split_name = "QPair.qsplit"
    1.35    val pair_iff  = QPair_iff
    1.36    val split_eq  = qsplit
    1.37    val fsplitI   = qsplitI
    1.38 @@ -88,10 +88,10 @@
    1.39  
    1.40  structure Quine_Sum =
    1.41    struct
    1.42 -  val sum       = Const("op <+>", [iT,iT]--->iT)
    1.43 -  val inl       = Const("QInl", iT-->iT)
    1.44 -  val inr       = Const("QInr", iT-->iT)
    1.45 -  val elim      = Const("qcase", [iT-->iT, iT-->iT, iT]--->iT)
    1.46 +  val sum       = Const("QPair.op <+>", [iT,iT]--->iT)
    1.47 +  val inl       = Const("QPair.QInl", iT-->iT)
    1.48 +  val inr       = Const("QPair.QInr", iT-->iT)
    1.49 +  val elim      = Const("QPair.qcase", [iT-->iT, iT-->iT, iT]--->iT)
    1.50    val case_inl  = qcase_QInl
    1.51    val case_inr  = qcase_QInr
    1.52    val inl_iff   = QInl_iff