/src/ZF/
drwxr-xr-x [up]
drwxr-xr-x AC
drwxr-xr-x Coind
drwxr-xr-x IMP
drwxr-xr-x Induct
drwxr-xr-x Integ
drwxr-xr-x Resid
drwxr-xr-x Tools
drwxr-xr-x UNITY
drwxr-xr-x ex
-rw-r--r-- 2002-02-15 12:07 +0100 2269 AC.ML
-rw-r--r-- 2002-02-15 12:07 +0100 481 AC.thy
-rw-r--r-- 2002-02-15 12:07 +0100 14951 Arith.ML
-rw-r--r-- 2002-02-15 12:07 +0100 1810 Arith.thy
-rw-r--r-- 2002-02-15 12:07 +0100 19072 ArithSimp.ML
-rw-r--r-- 2002-02-15 12:07 +0100 264 ArithSimp.thy
-rw-r--r-- 2002-02-15 12:07 +0100 3851 Bool.ML
-rw-r--r-- 2002-02-15 12:07 +0100 898 Bool.thy
-rw-r--r-- 2002-02-15 12:07 +0100 28544 Cardinal.ML
-rw-r--r-- 2002-02-15 12:07 +0100 1172 Cardinal.thy
-rw-r--r-- 2002-02-15 12:07 +0100 33209 CardinalArith.ML
-rw-r--r-- 2002-02-15 12:07 +0100 5169 CardinalArith.thy
-rw-r--r-- 2002-02-15 12:07 +0100 6696 Cardinal_AC.ML
-rw-r--r-- 2002-02-15 12:07 +0100 264 Cardinal_AC.thy
-rw-r--r-- 2002-02-15 12:07 +0100 3531 Datatype.ML
-rw-r--r-- 2002-02-15 12:07 +0100 385 Datatype.thy
-rw-r--r-- 2002-02-15 12:07 +0100 10946 Epsilon.ML
-rw-r--r-- 2002-02-15 12:07 +0100 987 Epsilon.thy
-rw-r--r-- 2002-02-15 12:07 +0100 3631 Fin.ML
-rw-r--r-- 2002-02-15 12:07 +0100 85 Fin.thy
-rw-r--r-- 2002-02-15 12:07 +0100 6229 Finite.ML
-rw-r--r-- 2002-02-15 12:07 +0100 938 Finite.thy
-rw-r--r-- 2002-02-15 12:07 +0100 9677 Fixedpt.ML
-rw-r--r-- 2002-02-15 12:07 +0100 567 Fixedpt.thy
-rw-r--r-- 2002-02-15 12:07 +0100 3214 Inductive.ML
-rw-r--r-- 2002-02-15 12:07 +0100 612 Inductive.thy
-rw-r--r-- 2002-02-15 12:07 +0100 4022 InfDatatype.ML
-rw-r--r-- 2002-02-15 12:07 +0100 53 InfDatatype.thy
-rw-r--r-- 2002-02-15 12:07 +0100 4263 IsaMakefile
-rw-r--r-- 2002-02-15 12:07 +0100 348 Let.ML
-rw-r--r-- 2002-02-15 12:07 +0100 775 Let.thy
-rw-r--r-- 2002-02-15 12:07 +0100 37746 List.ML
-rw-r--r-- 2002-02-15 12:07 +0100 3391 List.thy
-rw-r--r-- 2002-02-15 12:07 +0100 11464 ListFn.ML
-rw-r--r-- 2002-02-15 12:07 +0100 1607 ListFn.thy
-rw-r--r-- 2002-02-15 12:07 +0100 134 Main.ML
-rw-r--r-- 2002-02-15 12:07 +0100 2863 Main.thy
-rw-r--r-- 2002-02-15 12:07 +0100 61 Main_ZFC.ML
-rw-r--r-- 2002-02-15 12:07 +0100 43 Main_ZFC.thy
-rw-r--r-- 2002-02-15 12:07 +0100 6885 Nat.ML
-rw-r--r-- 2002-02-15 12:07 +0100 925 Nat.thy
-rw-r--r-- 2002-02-15 12:07 +0100 17373 Ord.ML
-rw-r--r-- 2002-02-15 12:07 +0100 737 Ord.thy
-rw-r--r-- 2002-02-15 12:07 +0100 3444 OrdQuant.ML
-rw-r--r-- 2002-02-15 12:07 +0100 5674 OrdQuant.thy
-rw-r--r-- 2002-02-15 12:07 +0100 21906 Order.ML
-rw-r--r-- 2002-02-15 12:07 +0100 1561 Order.thy
-rw-r--r-- 2002-02-15 12:07 +0100 14478 OrderArith.ML
-rw-r--r-- 2002-02-15 12:07 +0100 1187 OrderArith.thy
-rw-r--r-- 2002-02-15 12:07 +0100 32553 OrderType.ML
-rw-r--r-- 2002-02-15 12:07 +0100 1313 OrderType.thy
-rw-r--r-- 2002-02-15 12:07 +0100 20710 Ordinal.ML
-rw-r--r-- 2002-02-15 12:07 +0100 937 Ordinal.thy
-rw-r--r-- 2002-02-15 12:07 +0100 4784 Pair.ML
-rw-r--r-- 2002-02-15 12:07 +0100 59 Pair.thy
-rw-r--r-- 2002-02-15 12:07 +0100 17151 Perm.ML
-rw-r--r-- 2002-02-15 12:07 +0100 1043 Perm.thy
-rw-r--r-- 2002-02-15 12:07 +0100 7906 QPair.ML
-rw-r--r-- 2002-02-15 12:07 +0100 1667 QPair.thy
-rw-r--r-- 2002-02-15 12:07 +0100 6241 QUniv.ML
-rw-r--r-- 2002-02-15 12:07 +0100 561 QUniv.thy
-rw-r--r-- 2002-02-15 12:07 +0100 2389 README.html
-rw-r--r-- 2002-02-15 12:07 +0100 669 ROOT.ML
-rw-r--r-- 2002-02-15 12:07 +0100 1328 Rel.ML
-rw-r--r-- 2002-02-15 12:07 +0100 955 Rel.thy
-rw-r--r-- 2002-02-15 12:07 +0100 4787 Sum.ML
-rw-r--r-- 2002-02-15 12:07 +0100 776 Sum.thy
-rw-r--r-- 2002-02-15 12:07 +0100 8900 Trancl.ML
-rw-r--r-- 2002-02-15 12:07 +0100 514 Trancl.thy
-rw-r--r-- 2002-02-15 12:07 +0100 23600 Univ.ML
-rw-r--r-- 2002-02-15 12:07 +0100 1152 Univ.thy
-rw-r--r-- 2002-02-15 12:07 +0100 1199 Update.ML
-rw-r--r-- 2002-02-15 12:07 +0100 841 Update.thy
-rw-r--r-- 2002-02-15 12:07 +0100 11532 WF.ML
-rw-r--r-- 2002-02-15 12:07 +0100 1150 WF.thy
-rw-r--r-- 2002-02-15 12:07 +0100 14039 ZF.ML
-rw-r--r-- 2002-02-15 12:07 +0100 9596 ZF.thy
-rw-r--r-- 2002-02-15 12:07 +0100 13211 Zorn.ML
-rw-r--r-- 2002-02-15 12:07 +0100 1427 Zorn.thy
-rw-r--r-- 2002-02-15 12:07 +0100 1676 Zorn0.ML
-rw-r--r-- 2002-02-15 12:07 +0100 850 Zorn0.thy
-rw-r--r-- 2002-02-15 12:07 +0100 12291 arith.ML
-rw-r--r-- 2002-02-15 12:07 +0100 878 arith.thy
-rw-r--r-- 2002-02-15 12:07 +0100 8824 arith_data.ML
-rw-r--r-- 2002-02-15 12:07 +0100 4239 bool.ML
-rw-r--r-- 2002-02-15 12:07 +0100 767 bool.thy
-rw-r--r-- 2002-02-15 12:07 +0100 1769 co-inductive.ML
-rw-r--r-- 2002-02-15 12:07 +0100 1762 coinductive.ML
-rw-r--r-- 2002-02-15 12:07 +0100 84 coinductive.thy
-rw-r--r-- 2002-02-15 12:07 +0100 2033 datatype.ML
-rw-r--r-- 2002-02-15 12:07 +0100 194 datatype.thy
-rw-r--r-- 2002-02-15 12:07 +0100 5414 domrange.ML
-rw-r--r-- 2002-02-15 12:07 +0100 70 domrange.thy
-rw-r--r-- 2002-02-15 12:07 +0100 9962 epsilon.ML
-rw-r--r-- 2002-02-15 12:07 +0100 523 epsilon.thy
-rw-r--r-- 2002-02-15 12:07 +0100 17047 equalities.ML
-rw-r--r-- 2002-02-15 12:07 +0100 67 equalities.thy
-rw-r--r-- 2002-02-15 12:07 +0100 3482 fin.ML
-rw-r--r-- 2002-02-15 12:07 +0100 115 fin.thy
-rw-r--r-- 2002-02-15 12:07 +0100 11068 fixedpt.ML
-rw-r--r-- 2002-02-15 12:07 +0100 571 fixedpt.thy
-rw-r--r-- 2002-02-15 12:07 +0100 14527 func.ML
-rw-r--r-- 2002-02-15 12:07 +0100 73 func.thy
-rw-r--r-- 2002-02-15 12:07 +0100 5337 ind-syntax.ML
-rw-r--r-- 2002-02-15 12:07 +0100 6259 ind_syntax.ML
-rw-r--r-- 2002-02-15 12:07 +0100 7275 inductive.ML
-rw-r--r-- 2002-02-15 12:07 +0100 66 inductive.thy
-rw-r--r-- 2002-02-15 12:07 +0100 10794 intr-elim.ML
-rw-r--r-- 2002-02-15 12:07 +0100 2411 list.ML
-rw-r--r-- 2002-02-15 12:07 +0100 83 list.thy
-rw-r--r-- 2002-02-15 12:07 +0100 11464 listfn.ML
-rw-r--r-- 2002-02-15 12:07 +0100 1607 listfn.thy
-rw-r--r-- 2002-02-15 12:07 +0100 5138 mono.ML
-rw-r--r-- 2002-02-15 12:07 +0100 27 mono.thy
-rw-r--r-- 2002-02-15 12:07 +0100 6543 nat.ML
-rw-r--r-- 2002-02-15 12:07 +0100 629 nat.thy
-rw-r--r-- 2002-02-15 12:07 +0100 17373 ord.ML
-rw-r--r-- 2002-02-15 12:07 +0100 737 ord.thy
-rw-r--r-- 2002-02-15 12:07 +0100 4561 pair.ML
-rw-r--r-- 2002-02-15 12:07 +0100 47 pair.thy
-rw-r--r-- 2002-02-15 12:07 +0100 15282 perm.ML
-rw-r--r-- 2002-02-15 12:07 +0100 1066 perm.thy
-rw-r--r-- 2002-02-15 12:07 +0100 9009 qpair.ML
-rw-r--r-- 2002-02-15 12:07 +0100 1613 qpair.thy
-rw-r--r-- 2002-02-15 12:07 +0100 7679 quniv.ML
-rw-r--r-- 2002-02-15 12:07 +0100 357 quniv.thy
-rw-r--r-- 2002-02-15 12:07 +0100 8888 simpdata.ML
-rw-r--r-- 2002-02-15 12:07 +0100 4801 subset.ML
-rw-r--r-- 2002-02-15 12:07 +0100 58 subset.thy
-rw-r--r-- 2002-02-15 12:07 +0100 4635 sum.ML
-rw-r--r-- 2002-02-15 12:07 +0100 744 sum.thy
-rw-r--r-- 2002-02-15 12:07 +0100 6449 thy_syntax.ML
-rw-r--r-- 2002-02-15 12:07 +0100 6800 trancl.ML
-rw-r--r-- 2002-02-15 12:07 +0100 644 trancl.thy
-rw-r--r-- 2002-02-15 12:07 +0100 20259 univ.ML
-rw-r--r-- 2002-02-15 12:07 +0100 927 univ.thy
-rw-r--r-- 2002-02-15 12:07 +0100 10000 upair.ML
-rw-r--r-- 2002-02-15 12:07 +0100 287 upair.thy
-rw-r--r-- 2002-02-15 12:07 +0100 8775 wf.ML
-rw-r--r-- 2002-02-15 12:07 +0100 852 wf.thy
-rw-r--r-- 2002-02-15 12:07 +0100 14167 zf.ML
-rw-r--r-- 2002-02-15 12:07 +0100 7517 zf.thy