Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
ZF belongs to chapter FOL, following lib/html/library_index_content.template (i.e. "Documentation" area on website);
authorwenzelm
Sat, 27 Aug 2022 17:53:00 +0200
changeset 76006 c9d56340b56e
parent 76005 a9bbf075f431
child 76007 08288b406005
ZF belongs to chapter FOL, following lib/html/library_index_content.template (i.e. "Documentation" area on website);
ROOT file | annotate | diff | comparison | revisions
src/ZF/ROOT file | annotate | diff | comparison | revisions 
--- 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
--- 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 "
isabelle