This directory contains an integration of first-order set theory with
ACL2.  As a result, ACL2 can be used as a theorem prover for
Zermelo-Frankel set theory (ZF) with choice (so, ZFC); see :DOC zfc.

WARNING (March 2025): This is work in progress, so substantial changes
are possible.
