src/ZF/ROOT
changeset 48738 f8c1a5b9488f
parent 48487 94a9650f79fb
child 50574 0706797501a0
equal deleted inserted replaced
48737:f3bbb9ca57d6 48738:f8c1a5b9488f
     1 session ZF! in "." = Pure +
     1 session ZF = Pure +
     2   description {*
     2   description {*
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1995  University of Cambridge
     4     Copyright   1995  University of Cambridge
     5 
     5 
     6     Zermelo-Fraenkel Set Theory on top of classical First-Order Logic.
     6     Zermelo-Fraenkel Set Theory on top of classical First-Order Logic.
    11   theories
    11   theories
    12     Main
    12     Main
    13     Main_ZFC
    13     Main_ZFC
    14   files "document/root.tex"
    14   files "document/root.tex"
    15 
    15 
    16 session AC = ZF +
    16 session "ZF-AC" in AC = ZF +
    17   description {*
    17   description {*
    18     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    18     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    19     Copyright   1995  University of Cambridge
    19     Copyright   1995  University of Cambridge
    20 
    20 
    21     Proofs of AC-equivalences, due to Krzysztof Grabczewski.
    21     Proofs of AC-equivalences, due to Krzysztof Grabczewski.
    32     AC17_AC1
    32     AC17_AC1
    33     AC18_AC19
    33     AC18_AC19
    34     DC
    34     DC
    35   files "document/root.tex" "document/root.bib"
    35   files "document/root.tex" "document/root.bib"
    36 
    36 
    37 session Coind = ZF +
    37 session "ZF-Coind" in Coind = ZF +
    38   description {*
    38   description {*
    39     Author:     Jacob Frost, Cambridge University Computer Laboratory
    39     Author:     Jacob Frost, Cambridge University Computer Laboratory
    40     Copyright   1995  University of Cambridge
    40     Copyright   1995  University of Cambridge
    41 
    41 
    42     Coind -- A Coinduction Example.
    42     Coind -- A Coinduction Example.
    51         Report, Computer Lab, University of Cambridge (1995).
    51         Report, Computer Lab, University of Cambridge (1995).
    52   *}
    52   *}
    53   options [document = false]
    53   options [document = false]
    54   theories ECR
    54   theories ECR
    55 
    55 
    56 session Constructible = ZF +
    56 session "ZF-Constructible" in Constructible = ZF +
    57   description {* Inner Models, Absoluteness and Consistency Proofs. *}
    57   description {* Inner Models, Absoluteness and Consistency Proofs. *}
    58   options [document_graph]
    58   options [document_graph]
    59   theories DPow_absolute AC_in_L Rank_Separation
    59   theories DPow_absolute AC_in_L Rank_Separation
    60   files "document/root.tex" "document/root.bib"
    60   files "document/root.tex" "document/root.bib"
    61 
    61 
    62 session IMP = ZF +
    62 session "ZF-IMP" in IMP = ZF +
    63   description {*
    63   description {*
    64     Author:     Heiko Loetzbeyer & Robert Sandner, TUM
    64     Author:     Heiko Loetzbeyer & Robert Sandner, TUM
    65     Copyright   1994 TUM
    65     Copyright   1994 TUM
    66 
    66 
    67     Formalization of the denotational and operational semantics of a
    67     Formalization of the denotational and operational semantics of a
    75   *}
    75   *}
    76   options [document = false]
    76   options [document = false]
    77   theories Equiv
    77   theories Equiv
    78   files "document/root.tex" "document/root.bib"
    78   files "document/root.tex" "document/root.bib"
    79 
    79 
    80 session Induct = ZF +
    80 session "ZF-Induct" in Induct = ZF +
    81   description {*
    81   description {*
    82     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    82     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    83     Copyright   2001  University of Cambridge
    83     Copyright   2001  University of Cambridge
    84 
    84 
    85     Inductive definitions.
    85     Inductive definitions.
   106 
   106 
   107     Comb            (*Combinatory Logic example*)
   107     Comb            (*Combinatory Logic example*)
   108     Primrec         (*Primitive recursive functions*)
   108     Primrec         (*Primitive recursive functions*)
   109   files "document/root.tex"
   109   files "document/root.tex"
   110 
   110 
   111 session Resid = ZF +
   111 session "ZF-Resid" in Resid = ZF +
   112   description {*
   112   description {*
   113     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
   113     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
   114     Copyright   1995  University of Cambridge
   114     Copyright   1995  University of Cambridge
   115 
   115 
   116     Residuals -- a proof of the Church-Rosser Theorem for the
   116     Residuals -- a proof of the Church-Rosser Theorem for the
   122     J. Functional Programming 4(3) 1994, 371-394.
   122     J. Functional Programming 4(3) 1994, 371-394.
   123   *}
   123   *}
   124   options [document = false]
   124   options [document = false]
   125   theories Confluence
   125   theories Confluence
   126 
   126 
   127 session UNITY = ZF +
   127 session "ZF-UNITY" in UNITY = ZF +
   128   description {*
   128   description {*
   129     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
   129     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
   130     Copyright   1998  University of Cambridge
   130     Copyright   1998  University of Cambridge
   131 
   131 
   132     ZF/UNITY proofs.
   132     ZF/UNITY proofs.
   140     Guar
   140     Guar
   141 
   141 
   142     (*Prefix relation; the Allocator example*)
   142     (*Prefix relation; the Allocator example*)
   143     Distributor Merge ClientImpl AllocImpl
   143     Distributor Merge ClientImpl AllocImpl
   144 
   144 
   145 session ex = ZF +
   145 session "ZF-ex" in ex = ZF +
   146   description {*
   146   description {*
   147     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
   147     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
   148     Copyright   1993  University of Cambridge
   148     Copyright   1993  University of Cambridge
   149 
   149 
   150     Miscellaneous examples for Zermelo-Fraenkel Set Theory.
   150     Miscellaneous examples for Zermelo-Fraenkel Set Theory.