/src/ZF/Constructible/
drwxr-xr-x [up]
drwxr-xr-x document
-rw-r--r-- 2020-12-11 17:58 +0100 16924 AC_in_L.thy
-rw-r--r-- 2020-12-11 17:58 +0100 24244 DPow_absolute.thy
-rw-r--r-- 2020-12-11 17:58 +0100 39361 Datatype_absolute.thy
-rw-r--r-- 2020-12-11 17:58 +0100 35277 Formula.thy
-rw-r--r-- 2020-12-11 17:58 +0100 57329 Internalize.thy
-rw-r--r-- 2020-12-11 17:58 +0100 50862 L_axioms.thy
-rw-r--r-- 2020-12-11 17:58 +0100 1077 MetaExists.thy
-rw-r--r-- 2020-12-11 17:58 +0100 17336 Normal.thy
-rw-r--r-- 2020-12-11 17:58 +0100 37509 Rank.thy
-rw-r--r-- 2020-12-11 17:58 +0100 11307 Rank_Separation.thy
-rw-r--r-- 2020-12-11 17:58 +0100 17532 Rec_Separation.thy
-rw-r--r-- 2020-12-11 17:58 +0100 15912 Reflection.thy
-rw-r--r-- 2020-12-11 17:58 +0100 60149 Relative.thy
-rw-r--r-- 2020-12-11 17:58 +0100 44294 Satisfies_absolute.thy
-rw-r--r-- 2020-12-11 17:58 +0100 12888 Separation.thy
-rw-r--r-- 2020-12-11 17:58 +0100 13010 WF_absolute.thy
-rw-r--r-- 2020-12-11 17:58 +0100 14474 WFrec.thy
-rw-r--r-- 2020-12-11 17:58 +0100 9293 Wellorderings.thy