src/ZF/ROOT
changeset 66778 cf0187ca3a57
parent 66750 41fbe4a3aac9
child 66946 3d8fd98c7c86
equal deleted inserted replaced
66777:8df01b0db3e9 66778:cf0187ca3a57
     1 chapter ZF
     1 chapter ZF
     2 
     2 
     3 session ZF (main timing ZF) = Pure +
     3 session ZF (main timing) = Pure +
     4   description {*
     4   description {*
     5     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     5     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     6     Copyright   1995  University of Cambridge
     6     Copyright   1995  University of Cambridge
     7 
     7 
     8     Zermelo-Fraenkel Set Theory. This theory is the work of Martin Coen,
     8     Zermelo-Fraenkel Set Theory. This theory is the work of Martin Coen,
    47   theories
    47   theories
    48     ZF (global)
    48     ZF (global)
    49     ZFC (global)
    49     ZFC (global)
    50   document_files "root.tex"
    50   document_files "root.tex"
    51 
    51 
    52 session "ZF-AC" (ZF) in AC = ZF +
    52 session "ZF-AC" in AC = ZF +
    53   description {*
    53   description {*
    54     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    54     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    55     Copyright   1995  University of Cambridge
    55     Copyright   1995  University of Cambridge
    56 
    56 
    57     Proofs of AC-equivalences, due to Krzysztof Grabczewski.
    57     Proofs of AC-equivalences, due to Krzysztof Grabczewski.
    75     AC17_AC1
    75     AC17_AC1
    76     AC18_AC19
    76     AC18_AC19
    77     DC
    77     DC
    78   document_files "root.tex" "root.bib"
    78   document_files "root.tex" "root.bib"
    79 
    79 
    80 session "ZF-Coind" (ZF) in Coind = ZF +
    80 session "ZF-Coind" in Coind = ZF +
    81   description {*
    81   description {*
    82     Author:     Jacob Frost, Cambridge University Computer Laboratory
    82     Author:     Jacob Frost, Cambridge University Computer Laboratory
    83     Copyright   1995  University of Cambridge
    83     Copyright   1995  University of Cambridge
    84 
    84 
    85     Coind -- A Coinduction Example.
    85     Coind -- A Coinduction Example.
   101         http://www.cl.cam.ac.uk/Research/Reports/TR359-jf10008-co-induction-in-isabelle.dvi.gz
   101         http://www.cl.cam.ac.uk/Research/Reports/TR359-jf10008-co-induction-in-isabelle.dvi.gz
   102   *}
   102   *}
   103   options [document = false]
   103   options [document = false]
   104   theories ECR
   104   theories ECR
   105 
   105 
   106 session "ZF-Constructible" (ZF) in Constructible = ZF +
   106 session "ZF-Constructible" in Constructible = ZF +
   107   description {*
   107   description {*
   108     Relative Consistency of the Axiom of Choice:
   108     Relative Consistency of the Axiom of Choice:
   109     Inner Models, Absoluteness and Consistency Proofs.
   109     Inner Models, Absoluteness and Consistency Proofs.
   110 
   110 
   111     Gödel's proof of the relative consistency of the axiom of choice is
   111     Gödel's proof of the relative consistency of the axiom of choice is
   127     DPow_absolute
   127     DPow_absolute
   128     AC_in_L
   128     AC_in_L
   129     Rank_Separation
   129     Rank_Separation
   130   document_files "root.tex" "root.bib"
   130   document_files "root.tex" "root.bib"
   131 
   131 
   132 session "ZF-IMP" (ZF) in IMP = ZF +
   132 session "ZF-IMP" in IMP = ZF +
   133   description {*
   133   description {*
   134     Author:     Heiko Loetzbeyer & Robert Sandner, TUM
   134     Author:     Heiko Loetzbeyer & Robert Sandner, TUM
   135     Copyright   1994 TUM
   135     Copyright   1994 TUM
   136 
   136 
   137     Formalization of the denotational and operational semantics of a
   137     Formalization of the denotational and operational semantics of a
   146   theories Equiv
   146   theories Equiv
   147   document_files
   147   document_files
   148     "root.tex"
   148     "root.tex"
   149     "root.bib"
   149     "root.bib"
   150 
   150 
   151 session "ZF-Induct" (ZF) in Induct = ZF +
   151 session "ZF-Induct" in Induct = ZF +
   152   description {*
   152   description {*
   153     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
   153     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
   154     Copyright   2001  University of Cambridge
   154     Copyright   2001  University of Cambridge
   155 
   155 
   156     Inductive definitions.
   156     Inductive definitions.
   179     Primrec         (*Primitive recursive functions*)
   179     Primrec         (*Primitive recursive functions*)
   180   document_files
   180   document_files
   181     "root.bib"
   181     "root.bib"
   182     "root.tex"
   182     "root.tex"
   183 
   183 
   184 session "ZF-Resid" (ZF) in Resid = ZF +
   184 session "ZF-Resid" in Resid = ZF +
   185   description {*
   185   description {*
   186     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
   186     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
   187     Copyright   1995  University of Cambridge
   187     Copyright   1995  University of Cambridge
   188 
   188 
   189     Residuals -- a proof of the Church-Rosser Theorem for the
   189     Residuals -- a proof of the Church-Rosser Theorem for the
   199     http://www.cl.cam.ac.uk/ftp/papers/reports/TR364-or200-church-rosser-isabelle.ps.gz
   199     http://www.cl.cam.ac.uk/ftp/papers/reports/TR364-or200-church-rosser-isabelle.ps.gz
   200   *}
   200   *}
   201   options [document = false]
   201   options [document = false]
   202   theories Confluence
   202   theories Confluence
   203 
   203 
   204 session "ZF-UNITY" (timing ZF) in UNITY = "ZF-Induct" +
   204 session "ZF-UNITY" (timing) in UNITY = "ZF-Induct" +
   205   description {*
   205   description {*
   206     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
   206     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
   207     Copyright   1998  University of Cambridge
   207     Copyright   1998  University of Cambridge
   208 
   208 
   209     ZF/UNITY proofs.
   209     ZF/UNITY proofs.
   217     Guar
   217     Guar
   218 
   218 
   219     (*Prefix relation; the Allocator example*)
   219     (*Prefix relation; the Allocator example*)
   220     Distributor Merge ClientImpl AllocImpl
   220     Distributor Merge ClientImpl AllocImpl
   221 
   221 
   222 session "ZF-ex" (ZF) in ex = ZF +
   222 session "ZF-ex" in ex = ZF +
   223   description {*
   223   description {*
   224     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
   224     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
   225     Copyright   1993  University of Cambridge
   225     Copyright   1993  University of Cambridge
   226 
   226 
   227     Miscellaneous examples for Zermelo-Fraenkel Set Theory.
   227     Miscellaneous examples for Zermelo-Fraenkel Set Theory.