/src/ZF/
drwxr-xr-x [up]
drwxr-xr-x IMP
drwxr-xr-x ex
-rw-r--r-- 1994-12-23 16:49 +0100 1724 AC.ML
-rw-r--r-- 1994-12-23 16:49 +0100 339 AC.thy
-rw-r--r-- 1994-12-23 16:49 +0100 12522 Arith.ML
-rw-r--r-- 1994-12-23 16:49 +0100 877 Arith.thy
-rw-r--r-- 1994-12-23 16:49 +0100 4035 Bool.ML
-rw-r--r-- 1994-12-23 16:49 +0100 853 Bool.thy
-rw-r--r-- 1994-12-23 16:49 +0100 23557 Cardinal.ML
-rw-r--r-- 1994-12-23 16:49 +0100 894 Cardinal.thy
-rw-r--r-- 1994-12-23 16:49 +0100 28984 CardinalArith.ML
-rw-r--r-- 1994-12-23 16:49 +0100 1146 CardinalArith.thy
-rw-r--r-- 1994-12-23 16:49 +0100 6801 Cardinal_AC.ML
-rw-r--r-- 1994-12-23 16:49 +0100 257 Cardinal_AC.thy
-rw-r--r-- 1994-12-23 16:49 +0100 1976 Datatype.ML
-rw-r--r-- 1994-12-23 16:49 +0100 167 Datatype.thy
-rw-r--r-- 1994-12-23 16:49 +0100 9660 Epsilon.ML
-rw-r--r-- 1994-12-23 16:49 +0100 522 Epsilon.thy
-rw-r--r-- 1994-12-23 16:49 +0100 8878 EquivClass.ML
-rw-r--r-- 1994-12-23 16:49 +0100 660 EquivClass.thy
-rw-r--r-- 1994-12-23 16:49 +0100 3631 Fin.ML
-rw-r--r-- 1994-12-23 16:49 +0100 85 Fin.thy
-rw-r--r-- 1994-12-23 16:49 +0100 4802 Finite.ML
-rw-r--r-- 1994-12-23 16:49 +0100 750 Finite.thy
-rw-r--r-- 1994-12-23 16:49 +0100 10201 Fixedpt.ML
-rw-r--r-- 1994-12-23 16:49 +0100 570 Fixedpt.thy
-rw-r--r-- 1994-12-23 16:49 +0100 3595 Inductive.ML
-rw-r--r-- 1994-12-23 16:49 +0100 90 Inductive.thy
-rw-r--r-- 1994-12-23 16:49 +0100 4098 InfDatatype.ML
-rw-r--r-- 1994-12-23 16:49 +0100 53 InfDatatype.thy
-rw-r--r-- 1994-12-23 16:49 +0100 13001 List.ML
-rw-r--r-- 1994-12-23 16:49 +0100 1660 List.thy
-rw-r--r-- 1994-12-23 16:49 +0100 11464 ListFn.ML
-rw-r--r-- 1994-12-23 16:49 +0100 1607 ListFn.thy
-rw-r--r-- 1994-12-23 16:49 +0100 3285 Makefile
-rw-r--r-- 1994-12-23 16:49 +0100 6727 Nat.ML
-rw-r--r-- 1994-12-23 16:49 +0100 632 Nat.thy
-rw-r--r-- 1994-12-23 16:49 +0100 17373 Ord.ML
-rw-r--r-- 1994-12-23 16:49 +0100 737 Ord.thy
-rw-r--r-- 1994-12-23 16:49 +0100 21171 Order.ML
-rw-r--r-- 1994-12-23 16:49 +0100 1359 Order.thy
-rw-r--r-- 1994-12-23 16:49 +0100 9008 OrderArith.ML
-rw-r--r-- 1994-12-23 16:49 +0100 1040 OrderArith.thy
-rw-r--r-- 1994-12-23 16:49 +0100 8055 OrderType.ML
-rw-r--r-- 1994-12-23 16:49 +0100 512 OrderType.thy
-rw-r--r-- 1994-12-23 16:49 +0100 20057 Ordinal.ML
-rw-r--r-- 1994-12-23 16:49 +0100 841 Ordinal.thy
-rw-r--r-- 1994-12-23 16:49 +0100 4784 Pair.ML
-rw-r--r-- 1994-12-23 16:49 +0100 59 Pair.thy
-rw-r--r-- 1994-12-23 16:49 +0100 18368 Perm.ML
-rw-r--r-- 1994-12-23 16:49 +0100 1065 Perm.thy
-rw-r--r-- 1994-12-23 16:49 +0100 8513 QPair.ML
-rw-r--r-- 1994-12-23 16:49 +0100 1611 QPair.thy
-rw-r--r-- 1994-12-23 16:49 +0100 7428 QUniv.ML
-rw-r--r-- 1994-12-23 16:49 +0100 356 QUniv.thy
-rw-r--r-- 1994-12-23 16:49 +0100 1994 README
-rw-r--r-- 1994-12-23 16:49 +0100 1194 ROOT.ML
-rw-r--r-- 1994-12-23 16:49 +0100 1500 Rel.ML
-rw-r--r-- 1994-12-23 16:49 +0100 944 Rel.thy
-rw-r--r-- 1994-12-23 16:49 +0100 5131 Sum.ML
-rw-r--r-- 1994-12-23 16:49 +0100 743 Sum.thy
-rw-r--r-- 1994-12-23 16:49 +0100 6392 Trancl.ML
-rw-r--r-- 1994-12-23 16:49 +0100 513 Trancl.thy
-rw-r--r-- 1994-12-23 16:49 +0100 22302 Univ.ML
-rw-r--r-- 1994-12-23 16:49 +0100 930 Univ.thy
-rw-r--r-- 1994-12-23 16:49 +0100 11461 WF.ML
-rw-r--r-- 1994-12-23 16:49 +0100 1110 WF.thy
-rw-r--r-- 1994-12-23 16:49 +0100 15049 ZF.ML
-rw-r--r-- 1994-12-23 16:49 +0100 7627 ZF.thy
-rw-r--r-- 1994-12-23 16:49 +0100 14456 Zorn.ML
-rw-r--r-- 1994-12-23 16:49 +0100 1539 Zorn.thy
-rw-r--r-- 1994-12-23 16:49 +0100 1676 Zorn0.ML
-rw-r--r-- 1994-12-23 16:49 +0100 850 Zorn0.thy
-rw-r--r-- 1994-12-23 16:49 +0100 9418 add_ind_def.ML
-rw-r--r-- 1994-12-23 16:49 +0100 81 add_ind_def.thy
-rw-r--r-- 1994-12-23 16:49 +0100 12291 arith.ML
-rw-r--r-- 1994-12-23 16:49 +0100 878 arith.thy
-rw-r--r-- 1994-12-23 16:49 +0100 4239 bool.ML
-rw-r--r-- 1994-12-23 16:49 +0100 767 bool.thy
-rw-r--r-- 1994-12-23 16:49 +0100 1769 co-inductive.ML
-rw-r--r-- 1994-12-23 16:49 +0100 1762 coinductive.ML
-rw-r--r-- 1994-12-23 16:49 +0100 84 coinductive.thy
-rw-r--r-- 1994-12-23 16:49 +0100 2843 constructor.ML
-rw-r--r-- 1994-12-23 16:49 +0100 69 constructor.thy
-rw-r--r-- 1994-12-23 16:49 +0100 2033 datatype.ML
-rw-r--r-- 1994-12-23 16:49 +0100 194 datatype.thy
-rw-r--r-- 1994-12-23 16:49 +0100 6302 domrange.ML
-rw-r--r-- 1994-12-23 16:49 +0100 73 domrange.thy
-rw-r--r-- 1994-12-23 16:49 +0100 9962 epsilon.ML
-rw-r--r-- 1994-12-23 16:49 +0100 523 epsilon.thy
-rw-r--r-- 1994-12-23 16:49 +0100 11785 equalities.ML
-rw-r--r-- 1994-12-23 16:49 +0100 68 equalities.thy
-rw-r--r-- 1994-12-23 16:49 +0100 3482 fin.ML
-rw-r--r-- 1994-12-23 16:49 +0100 115 fin.thy
-rw-r--r-- 1994-12-23 16:49 +0100 11068 fixedpt.ML
-rw-r--r-- 1994-12-23 16:49 +0100 571 fixedpt.thy
-rw-r--r-- 1994-12-23 16:49 +0100 12417 func.ML
-rw-r--r-- 1994-12-23 16:49 +0100 77 func.thy
-rw-r--r-- 1994-12-23 16:49 +0100 5337 ind-syntax.ML
-rw-r--r-- 1994-12-23 16:49 +0100 4797 ind_syntax.ML
-rw-r--r-- 1994-12-23 16:49 +0100 64 ind_syntax.thy
-rw-r--r-- 1994-12-23 16:49 +0100 7238 indrule.ML
-rw-r--r-- 1994-12-23 16:49 +0100 81 indrule.thy
-rw-r--r-- 1994-12-23 16:49 +0100 7275 inductive.ML
-rw-r--r-- 1994-12-23 16:49 +0100 66 inductive.thy
-rw-r--r-- 1994-12-23 16:49 +0100 10794 intr-elim.ML
-rw-r--r-- 1994-12-23 16:49 +0100 6065 intr_elim.ML
-rw-r--r-- 1994-12-23 16:49 +0100 70 intr_elim.thy
-rw-r--r-- 1994-12-23 16:49 +0100 2411 list.ML
-rw-r--r-- 1994-12-23 16:49 +0100 83 list.thy
-rw-r--r-- 1994-12-23 16:49 +0100 11464 listfn.ML
-rw-r--r-- 1994-12-23 16:49 +0100 1607 listfn.thy
-rw-r--r-- 1994-12-23 16:49 +0100 5630 mono.ML
-rw-r--r-- 1994-12-23 16:49 +0100 63 mono.thy
-rw-r--r-- 1994-12-23 16:49 +0100 6543 nat.ML
-rw-r--r-- 1994-12-23 16:49 +0100 629 nat.thy
-rw-r--r-- 1994-12-23 16:49 +0100 17373 ord.ML
-rw-r--r-- 1994-12-23 16:49 +0100 737 ord.thy
-rw-r--r-- 1994-12-23 16:49 +0100 6315 pair.ML
-rw-r--r-- 1994-12-23 16:49 +0100 59 pair.thy
-rw-r--r-- 1994-12-23 16:49 +0100 15282 perm.ML
-rw-r--r-- 1994-12-23 16:49 +0100 1066 perm.thy
-rw-r--r-- 1994-12-23 16:49 +0100 9009 qpair.ML
-rw-r--r-- 1994-12-23 16:49 +0100 1613 qpair.thy
-rw-r--r-- 1994-12-23 16:49 +0100 7679 quniv.ML
-rw-r--r-- 1994-12-23 16:49 +0100 357 quniv.thy
-rw-r--r-- 1994-12-23 16:49 +0100 2793 simpdata.ML
-rw-r--r-- 1994-12-23 16:49 +0100 62 simpdata.thy
-rw-r--r-- 1994-12-23 16:49 +0100 6105 subset.ML
-rw-r--r-- 1994-12-23 16:49 +0100 61 subset.thy
-rw-r--r-- 1994-12-23 16:49 +0100 4635 sum.ML
-rw-r--r-- 1994-12-23 16:49 +0100 744 sum.thy
-rw-r--r-- 1994-12-23 16:49 +0100 6111 thy_syntax.ML
-rw-r--r-- 1994-12-23 16:49 +0100 6800 trancl.ML
-rw-r--r-- 1994-12-23 16:49 +0100 644 trancl.thy
-rw-r--r-- 1994-12-23 16:49 +0100 20259 univ.ML
-rw-r--r-- 1994-12-23 16:49 +0100 927 univ.thy
-rw-r--r-- 1994-12-23 16:49 +0100 10282 upair.ML
-rw-r--r-- 1994-12-23 16:49 +0100 55 upair.thy
-rw-r--r-- 1994-12-23 16:49 +0100 8775 wf.ML
-rw-r--r-- 1994-12-23 16:49 +0100 852 wf.thy
-rw-r--r-- 1994-12-23 16:49 +0100 14167 zf.ML
-rw-r--r-- 1994-12-23 16:49 +0100 7517 zf.thy