discontinued somewhat pointless session group: -g ZF may be replaced by -D ~~/src/ZF;
authorwenzelm
Sat Oct 07 15:21:25 2017 +0200 (9 months ago)
changeset 66778cf0187ca3a57
parent 66777 8df01b0db3e9
child 66779 8645d56f96e1
discontinued somewhat pointless session group: -g ZF may be replaced by -D ~~/src/ZF;
src/ZF/ROOT
     1.1 --- a/src/ZF/ROOT	Sat Oct 07 14:57:54 2017 +0200
     1.2 +++ b/src/ZF/ROOT	Sat Oct 07 15:21:25 2017 +0200
     1.3 @@ -1,6 +1,6 @@
     1.4  chapter ZF
     1.5  
     1.6 -session ZF (main timing ZF) = Pure +
     1.7 +session ZF (main timing) = Pure +
     1.8    description {*
     1.9      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    1.10      Copyright   1995  University of Cambridge
    1.11 @@ -49,7 +49,7 @@
    1.12      ZFC (global)
    1.13    document_files "root.tex"
    1.14  
    1.15 -session "ZF-AC" (ZF) in AC = ZF +
    1.16 +session "ZF-AC" in AC = ZF +
    1.17    description {*
    1.18      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    1.19      Copyright   1995  University of Cambridge
    1.20 @@ -77,7 +77,7 @@
    1.21      DC
    1.22    document_files "root.tex" "root.bib"
    1.23  
    1.24 -session "ZF-Coind" (ZF) in Coind = ZF +
    1.25 +session "ZF-Coind" in Coind = ZF +
    1.26    description {*
    1.27      Author:     Jacob Frost, Cambridge University Computer Laboratory
    1.28      Copyright   1995  University of Cambridge
    1.29 @@ -103,7 +103,7 @@
    1.30    options [document = false]
    1.31    theories ECR
    1.32  
    1.33 -session "ZF-Constructible" (ZF) in Constructible = ZF +
    1.34 +session "ZF-Constructible" in Constructible = ZF +
    1.35    description {*
    1.36      Relative Consistency of the Axiom of Choice:
    1.37      Inner Models, Absoluteness and Consistency Proofs.
    1.38 @@ -129,7 +129,7 @@
    1.39      Rank_Separation
    1.40    document_files "root.tex" "root.bib"
    1.41  
    1.42 -session "ZF-IMP" (ZF) in IMP = ZF +
    1.43 +session "ZF-IMP" in IMP = ZF +
    1.44    description {*
    1.45      Author:     Heiko Loetzbeyer & Robert Sandner, TUM
    1.46      Copyright   1994 TUM
    1.47 @@ -148,7 +148,7 @@
    1.48      "root.tex"
    1.49      "root.bib"
    1.50  
    1.51 -session "ZF-Induct" (ZF) in Induct = ZF +
    1.52 +session "ZF-Induct" in Induct = ZF +
    1.53    description {*
    1.54      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    1.55      Copyright   2001  University of Cambridge
    1.56 @@ -181,7 +181,7 @@
    1.57      "root.bib"
    1.58      "root.tex"
    1.59  
    1.60 -session "ZF-Resid" (ZF) in Resid = ZF +
    1.61 +session "ZF-Resid" in Resid = ZF +
    1.62    description {*
    1.63      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    1.64      Copyright   1995  University of Cambridge
    1.65 @@ -201,7 +201,7 @@
    1.66    options [document = false]
    1.67    theories Confluence
    1.68  
    1.69 -session "ZF-UNITY" (timing ZF) in UNITY = "ZF-Induct" +
    1.70 +session "ZF-UNITY" (timing) in UNITY = "ZF-Induct" +
    1.71    description {*
    1.72      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    1.73      Copyright   1998  University of Cambridge
    1.74 @@ -219,7 +219,7 @@
    1.75      (*Prefix relation; the Allocator example*)
    1.76      Distributor Merge ClientImpl AllocImpl
    1.77  
    1.78 -session "ZF-ex" (ZF) in ex = ZF +
    1.79 +session "ZF-ex" in ex = ZF +
    1.80    description {*
    1.81      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    1.82      Copyright   1993  University of Cambridge