# HG changeset patch
# User wenzelm
# Date 1661615580 -7200
# Node ID c9d56340b56e691cefc6a28873643e07cd3bacf5
# Parent  a9bbf075f4319e920a22a1c0a5b763b6575f2089
ZF belongs to chapter FOL, following lib/html/library_index_content.template (i.e. "Documentation" area on website);

diff -r a9bbf075f431 -r c9d56340b56e ROOT
--- a/ROOT	Sat Aug 27 17:46:58 2022 +0200
+++ b/ROOT	Sat Aug 27 17:53:00 2022 +0200
@@ -6,18 +6,11 @@
     that of the HOL System (https://www.cl.cam.ac.uk/Research/HVG/HOL).
   "
 
-chapter_definition ZF
-  description "
-    Zermelo-Fraenkel set theory.
-
-    Isabelle/ZF offers a formulation of Zermelo-Fraenkel set theory on top of
-    Isabelle/FOL.
-  "
-
 chapter_definition FOL
   description "
     First-Order Logic with some variations: single-sorted vs. many-sorted
-    (polymorphic), classical vs. intuitionistic, domain-theory (LCF).
+    (polymorphic), classical vs. intuitionistic, domain-theory (LCF) vs.
+    set-theory (ZF).
   "
 
 chapter_definition Pure
diff -r a9bbf075f431 -r c9d56340b56e src/ZF/ROOT
--- a/src/ZF/ROOT	Sat Aug 27 17:46:58 2022 +0200
+++ b/src/ZF/ROOT	Sat Aug 27 17:53:00 2022 +0200
@@ -1,4 +1,4 @@
-chapter ZF
+chapter FOL
 
 session ZF (main timing) = Pure +
   description "