| author | nipkow | 
| Sun, 28 May 2017 15:46:26 +0200 | |
| changeset 65955 | 0616ba637b14 | 
| 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: 
35762 
diff
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  |