src/ZF/ROOT
changeset 48483 9bfb6978eb80
parent 48462 424fd5364f15
child 48487 94a9650f79fb
equal deleted inserted replaced
48482:45137257399a 48483:9bfb6978eb80
     6     Zermelo-Fraenkel Set Theory on top of classical First-Order Logic.
     6     Zermelo-Fraenkel Set Theory on top of classical First-Order Logic.
     7 
     7 
     8     This theory is the work of Martin Coen, Philippe Noel and Lawrence Paulson.
     8     This theory is the work of Martin Coen, Philippe Noel and Lawrence Paulson.
     9   *}
     9   *}
    10   options [document_graph]
    10   options [document_graph]
    11   theories Main Main_ZFC
    11   theories
       
    12     Main
       
    13     Main_ZFC
    12   files "document/root.tex"
    14   files "document/root.tex"
    13 
    15 
    14 session AC = ZF +
    16 session AC = ZF +
    15   description {*
    17   description {*
    16     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    18     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    17     Copyright   1995  University of Cambridge
    19     Copyright   1995  University of Cambridge
    18 
    20 
    19     Proofs of AC-equivalences, due to Krzysztof Grabczewski.
    21     Proofs of AC-equivalences, due to Krzysztof Grabczewski.
    20   *}
    22   *}
    21   options [document_graph]
    23   options [document_graph]
    22   theories WO6_WO1 WO1_WO7 AC7_AC9 WO1_AC AC15_WO6
    24   theories
    23     WO2_AC16 AC16_WO4 AC17_AC1 AC18_AC19 DC
    25     WO6_WO1
       
    26     WO1_WO7
       
    27     AC7_AC9
       
    28     WO1_AC
       
    29     AC15_WO6
       
    30     WO2_AC16
       
    31     AC16_WO4
       
    32     AC17_AC1
       
    33     AC18_AC19
       
    34     DC
    24   files "document/root.tex" "document/root.bib"
    35   files "document/root.tex" "document/root.bib"
    25 
    36 
    26 session Coind = ZF +
    37 session Coind = ZF +
    27   description {*
    38   description {*
    28     Author:     Jacob Frost, Cambridge University Computer Laboratory
    39     Author:     Jacob Frost, Cambridge University Computer Laboratory
    37 
    48 
    38     Written up as
    49     Written up as
    39         Jacob Frost, A Case Study of Co_induction in Isabelle
    50         Jacob Frost, A Case Study of Co_induction in Isabelle
    40         Report, Computer Lab, University of Cambridge (1995).
    51         Report, Computer Lab, University of Cambridge (1995).
    41   *}
    52   *}
       
    53   options [document = false]
    42   theories ECR
    54   theories ECR
    43 
    55 
    44 session Constructible = ZF +
    56 session Constructible = ZF +
    45   description {* Inner Models, Absoluteness and Consistency Proofs. *}
    57   description {* Inner Models, Absoluteness and Consistency Proofs. *}
    46   options [document_graph]
    58   options [document_graph]
    59     chapters 2 and 5 of
    71     chapters 2 and 5 of
    60 
    72 
    61     Glynn Winskel. The Formal Semantics of Programming Languages.
    73     Glynn Winskel. The Formal Semantics of Programming Languages.
    62     MIT Press, 1993.
    74     MIT Press, 1993.
    63   *}
    75   *}
       
    76   options [document = false]
    64   theories Equiv
    77   theories Equiv
    65   files "document/root.tex" "document/root.bib"
    78   files "document/root.tex" "document/root.bib"
    66 
    79 
    67 session Induct = ZF +
    80 session Induct = ZF +
    68   description {*
    81   description {*
   106     By Ole Rasmussen, following the Coq proof given in
   119     By Ole Rasmussen, following the Coq proof given in
   107 
   120 
   108     Gerard Huet.  Residual Theory in Lambda-Calculus: A Formal Development.
   121     Gerard Huet.  Residual Theory in Lambda-Calculus: A Formal Development.
   109     J. Functional Programming 4(3) 1994, 371-394.
   122     J. Functional Programming 4(3) 1994, 371-394.
   110   *}
   123   *}
       
   124   options [document = false]
   111   theories Confluence
   125   theories Confluence
   112 
   126 
   113 session UNITY = ZF +
   127 session UNITY = ZF +
   114   description {*
   128   description {*
   115     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
   129     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
   116     Copyright   1998  University of Cambridge
   130     Copyright   1998  University of Cambridge
   117 
   131 
   118     ZF/UNITY proofs.
   132     ZF/UNITY proofs.
   119   *}
   133   *}
       
   134   options [document = false]
   120   theories
   135   theories
   121     (*Simple examples: no composition*)
   136     (*Simple examples: no composition*)
   122     Mutex
   137     Mutex
   123 
   138 
   124     (*Basic meta-theory*)
   139     (*Basic meta-theory*)
   132     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
   147     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
   133     Copyright   1993  University of Cambridge
   148     Copyright   1993  University of Cambridge
   134 
   149 
   135     Miscellaneous examples for Zermelo-Fraenkel Set Theory.
   150     Miscellaneous examples for Zermelo-Fraenkel Set Theory.
   136   *}
   151   *}
       
   152   options [document = false]
   137   theories
   153   theories
   138     misc
   154     misc
   139     Ring             (*abstract algebra*)
   155     Ring             (*abstract algebra*)
   140     Commutation      (*abstract Church-Rosser theory*)
   156     Commutation      (*abstract Church-Rosser theory*)
   141     Primes           (*GCD theory*)
   157     Primes           (*GCD theory*)