| author | wenzelm | 
| Wed, 11 Sep 2024 23:07:18 +0200 | |
| changeset 80865 | 7c20c207af48 | 
| parent 65449 | c82e63b11b8b | 
| permissions | -rw-r--r-- | 
| 65449 
c82e63b11b8b
clarified main ZF.thy / ZFC.thy, and avoid name clash with global HOL/Main.thy;
 wenzelm parents: 
35762diff
changeset | 1 | theory ZFC imports ZF InfDatatype | 
| 35762 | 2 | begin | 
| 12552 
d2d2ab3f1f37
separation of the AC part of Main into Main_ZFC, plus a few new lemmas
 paulson parents: diff
changeset | 3 | |
| 
d2d2ab3f1f37
separation of the AC part of Main into Main_ZFC, plus a few new lemmas
 paulson parents: diff
changeset | 4 | end |