/src/ZF/
drwxr-xr-x [up]
drwxr-xr-x AC
drwxr-xr-x Coind
drwxr-xr-x IMP
drwxr-xr-x Resid
drwxr-xr-x ex
-rw-r--r-- 1995-05-10 08:38 +0200 1856 AC.ML
-rw-r--r-- 1995-05-10 08:38 +0200 339 AC.thy
-rw-r--r-- 1995-05-10 08:38 +0200 12522 Arith.ML
-rw-r--r-- 1995-05-10 08:38 +0200 877 Arith.thy
-rw-r--r-- 1995-05-10 08:38 +0200 4035 Bool.ML
-rw-r--r-- 1995-05-10 08:38 +0200 853 Bool.thy
-rw-r--r-- 1995-05-10 08:38 +0200 24125 Cardinal.ML
-rw-r--r-- 1995-05-10 08:38 +0200 894 Cardinal.thy
-rw-r--r-- 1995-05-10 08:38 +0200 28313 CardinalArith.ML
-rw-r--r-- 1995-05-10 08:38 +0200 1133 CardinalArith.thy
-rw-r--r-- 1995-05-10 08:38 +0200 7091 Cardinal_AC.ML
-rw-r--r-- 1995-05-10 08:38 +0200 257 Cardinal_AC.thy
-rw-r--r-- 1995-05-10 08:38 +0200 1976 Datatype.ML
-rw-r--r-- 1995-05-10 08:38 +0200 167 Datatype.thy
-rw-r--r-- 1995-05-10 08:38 +0200 9660 Epsilon.ML
-rw-r--r-- 1995-05-10 08:38 +0200 522 Epsilon.thy
-rw-r--r-- 1995-05-10 08:38 +0200 8730 EquivClass.ML
-rw-r--r-- 1995-05-10 08:38 +0200 660 EquivClass.thy
-rw-r--r-- 1995-05-10 08:38 +0200 3631 Fin.ML
-rw-r--r-- 1995-05-10 08:38 +0200 85 Fin.thy
-rw-r--r-- 1995-05-10 08:38 +0200 4802 Finite.ML
-rw-r--r-- 1995-05-10 08:38 +0200 750 Finite.thy
-rw-r--r-- 1995-05-10 08:38 +0200 10201 Fixedpt.ML
-rw-r--r-- 1995-05-10 08:38 +0200 570 Fixedpt.thy
-rw-r--r-- 1995-05-10 08:38 +0200 3587 Inductive.ML
-rw-r--r-- 1995-05-10 08:38 +0200 90 Inductive.thy
-rw-r--r-- 1995-05-10 08:38 +0200 4098 InfDatatype.ML
-rw-r--r-- 1995-05-10 08:38 +0200 53 InfDatatype.thy
-rw-r--r-- 1995-05-10 08:38 +0200 332 Let.ML
-rw-r--r-- 1995-05-10 08:38 +0200 762 Let.thy
-rw-r--r-- 1995-05-10 08:38 +0200 13030 List.ML
-rw-r--r-- 1995-05-10 08:38 +0200 1660 List.thy
-rw-r--r-- 1995-05-10 08:38 +0200 11464 ListFn.ML
-rw-r--r-- 1995-05-10 08:38 +0200 1607 ListFn.thy
-rw-r--r-- 1995-05-10 08:38 +0200 3462 Makefile
-rw-r--r-- 1995-05-10 08:38 +0200 6727 Nat.ML
-rw-r--r-- 1995-05-10 08:38 +0200 632 Nat.thy
-rw-r--r-- 1995-05-10 08:38 +0200 17373 Ord.ML
-rw-r--r-- 1995-05-10 08:38 +0200 737 Ord.thy
-rw-r--r-- 1995-05-10 08:38 +0200 22047 Order.ML
-rw-r--r-- 1995-05-10 08:38 +0200 1359 Order.thy
-rw-r--r-- 1995-05-10 08:38 +0200 15361 OrderArith.ML
-rw-r--r-- 1995-05-10 08:38 +0200 1040 OrderArith.thy
-rw-r--r-- 1995-05-10 08:38 +0200 33904 OrderType.ML
-rw-r--r-- 1995-05-10 08:38 +0200 1136 OrderType.thy
-rw-r--r-- 1995-05-10 08:38 +0200 21830 Ordinal.ML
-rw-r--r-- 1995-05-10 08:38 +0200 848 Ordinal.thy
-rw-r--r-- 1995-05-10 08:38 +0200 4784 Pair.ML
-rw-r--r-- 1995-05-10 08:38 +0200 59 Pair.thy
-rw-r--r-- 1995-05-10 08:38 +0200 18826 Perm.ML
-rw-r--r-- 1995-05-10 08:38 +0200 1065 Perm.thy
-rw-r--r-- 1995-05-10 08:38 +0200 9300 QPair.ML
-rw-r--r-- 1995-05-10 08:38 +0200 1658 QPair.thy
-rw-r--r-- 1995-05-10 08:38 +0200 8001 QUniv.ML
-rw-r--r-- 1995-05-10 08:38 +0200 356 QUniv.thy
-rw-r--r-- 1995-05-10 08:38 +0200 2556 README
-rw-r--r-- 1995-05-10 08:38 +0200 1209 ROOT.ML
-rw-r--r-- 1995-05-10 08:38 +0200 1500 Rel.ML
-rw-r--r-- 1995-05-10 08:38 +0200 944 Rel.thy
-rw-r--r-- 1995-05-10 08:38 +0200 5671 Sum.ML
-rw-r--r-- 1995-05-10 08:38 +0200 740 Sum.thy
-rw-r--r-- 1995-05-10 08:38 +0200 6392 Trancl.ML
-rw-r--r-- 1995-05-10 08:38 +0200 513 Trancl.thy
-rw-r--r-- 1995-05-10 08:38 +0200 21867 Univ.ML
-rw-r--r-- 1995-05-10 08:38 +0200 930 Univ.thy
-rw-r--r-- 1995-05-10 08:38 +0200 11461 WF.ML
-rw-r--r-- 1995-05-10 08:38 +0200 1109 WF.thy
-rw-r--r-- 1995-05-10 08:38 +0200 15157 ZF.ML
-rw-r--r-- 1995-05-10 08:38 +0200 8723 ZF.thy
-rw-r--r-- 1995-05-10 08:38 +0200 14420 Zorn.ML
-rw-r--r-- 1995-05-10 08:38 +0200 1539 Zorn.thy
-rw-r--r-- 1995-05-10 08:38 +0200 1676 Zorn0.ML
-rw-r--r-- 1995-05-10 08:38 +0200 850 Zorn0.thy
-rw-r--r-- 1995-05-10 08:38 +0200 9430 add_ind_def.ML
-rw-r--r-- 1995-05-10 08:38 +0200 81 add_ind_def.thy
-rw-r--r-- 1995-05-10 08:38 +0200 12291 arith.ML
-rw-r--r-- 1995-05-10 08:38 +0200 878 arith.thy
-rw-r--r-- 1995-05-10 08:38 +0200 4239 bool.ML
-rw-r--r-- 1995-05-10 08:38 +0200 767 bool.thy
-rw-r--r-- 1995-05-10 08:38 +0200 1769 co-inductive.ML
-rw-r--r-- 1995-05-10 08:38 +0200 1762 coinductive.ML
-rw-r--r-- 1995-05-10 08:38 +0200 84 coinductive.thy
-rw-r--r-- 1995-05-10 08:38 +0200 2943 constructor.ML
-rw-r--r-- 1995-05-10 08:38 +0200 69 constructor.thy
-rw-r--r-- 1995-05-10 08:38 +0200 2033 datatype.ML
-rw-r--r-- 1995-05-10 08:38 +0200 194 datatype.thy
-rw-r--r-- 1995-05-10 08:38 +0200 6302 domrange.ML
-rw-r--r-- 1995-05-10 08:38 +0200 73 domrange.thy
-rw-r--r-- 1995-05-10 08:38 +0200 9962 epsilon.ML
-rw-r--r-- 1995-05-10 08:38 +0200 523 epsilon.thy
-rw-r--r-- 1995-05-10 08:38 +0200 12068 equalities.ML
-rw-r--r-- 1995-05-10 08:38 +0200 68 equalities.thy
-rw-r--r-- 1995-05-10 08:38 +0200 3482 fin.ML
-rw-r--r-- 1995-05-10 08:38 +0200 115 fin.thy
-rw-r--r-- 1995-05-10 08:38 +0200 11068 fixedpt.ML
-rw-r--r-- 1995-05-10 08:38 +0200 571 fixedpt.thy
-rw-r--r-- 1995-05-10 08:38 +0200 12423 func.ML
-rw-r--r-- 1995-05-10 08:38 +0200 77 func.thy
-rw-r--r-- 1995-05-10 08:38 +0200 5337 ind-syntax.ML
-rw-r--r-- 1995-05-10 08:38 +0200 4797 ind_syntax.ML
-rw-r--r-- 1995-05-10 08:38 +0200 64 ind_syntax.thy
-rw-r--r-- 1995-05-10 08:38 +0200 7265 indrule.ML
-rw-r--r-- 1995-05-10 08:38 +0200 81 indrule.thy
-rw-r--r-- 1995-05-10 08:38 +0200 7275 inductive.ML
-rw-r--r-- 1995-05-10 08:38 +0200 66 inductive.thy
-rw-r--r-- 1995-05-10 08:38 +0200 10794 intr-elim.ML
-rw-r--r-- 1995-05-10 08:38 +0200 6074 intr_elim.ML
-rw-r--r-- 1995-05-10 08:38 +0200 70 intr_elim.thy
-rw-r--r-- 1995-05-10 08:38 +0200 2411 list.ML
-rw-r--r-- 1995-05-10 08:38 +0200 83 list.thy
-rw-r--r-- 1995-05-10 08:38 +0200 11464 listfn.ML
-rw-r--r-- 1995-05-10 08:38 +0200 1607 listfn.thy
-rw-r--r-- 1995-05-10 08:38 +0200 5630 mono.ML
-rw-r--r-- 1995-05-10 08:38 +0200 63 mono.thy
-rw-r--r-- 1995-05-10 08:38 +0200 6543 nat.ML
-rw-r--r-- 1995-05-10 08:38 +0200 629 nat.thy
-rw-r--r-- 1995-05-10 08:38 +0200 17373 ord.ML
-rw-r--r-- 1995-05-10 08:38 +0200 737 ord.thy
-rw-r--r-- 1995-05-10 08:38 +0200 6974 pair.ML
-rw-r--r-- 1995-05-10 08:38 +0200 59 pair.thy
-rw-r--r-- 1995-05-10 08:38 +0200 15282 perm.ML
-rw-r--r-- 1995-05-10 08:38 +0200 1066 perm.thy
-rw-r--r-- 1995-05-10 08:38 +0200 9009 qpair.ML
-rw-r--r-- 1995-05-10 08:38 +0200 1613 qpair.thy
-rw-r--r-- 1995-05-10 08:38 +0200 7679 quniv.ML
-rw-r--r-- 1995-05-10 08:38 +0200 357 quniv.thy
-rw-r--r-- 1995-05-10 08:38 +0200 3001 simpdata.ML
-rw-r--r-- 1995-05-10 08:38 +0200 78 simpdata.thy
-rw-r--r-- 1995-05-10 08:38 +0200 6105 subset.ML
-rw-r--r-- 1995-05-10 08:38 +0200 61 subset.thy
-rw-r--r-- 1995-05-10 08:38 +0200 4635 sum.ML
-rw-r--r-- 1995-05-10 08:38 +0200 744 sum.thy
-rw-r--r-- 1995-05-10 08:38 +0200 6111 thy_syntax.ML
-rw-r--r-- 1995-05-10 08:38 +0200 6800 trancl.ML
-rw-r--r-- 1995-05-10 08:38 +0200 644 trancl.thy
-rw-r--r-- 1995-05-10 08:38 +0200 20259 univ.ML
-rw-r--r-- 1995-05-10 08:38 +0200 927 univ.thy
-rw-r--r-- 1995-05-10 08:38 +0200 10494 upair.ML
-rw-r--r-- 1995-05-10 08:38 +0200 55 upair.thy
-rw-r--r-- 1995-05-10 08:38 +0200 8775 wf.ML
-rw-r--r-- 1995-05-10 08:38 +0200 852 wf.thy
-rw-r--r-- 1995-05-10 08:38 +0200 14167 zf.ML
-rw-r--r-- 1995-05-10 08:38 +0200 7517 zf.thy