/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-05-31 07:53 +0200 1953 AC.thy
-rw-r--r-- 2002-05-31 07:53 +0200 17405 Arith.thy
-rw-r--r-- 2002-05-31 07:53 +0200 19072 ArithSimp.ML
-rw-r--r-- 2002-05-31 07:53 +0200 264 ArithSimp.thy
-rw-r--r-- 2002-05-31 07:53 +0200 3851 Bool.ML
-rw-r--r-- 2002-05-31 07:53 +0200 898 Bool.thy
-rw-r--r-- 2002-05-31 07:53 +0200 28767 Cardinal.ML
-rw-r--r-- 2002-05-31 07:53 +0200 1172 Cardinal.thy
-rw-r--r-- 2002-05-31 07:53 +0200 33215 CardinalArith.ML
-rw-r--r-- 2002-05-31 07:53 +0200 6502 CardinalArith.thy
-rw-r--r-- 2002-05-31 07:53 +0200 5993 Cardinal_AC.thy
-rw-r--r-- 2002-05-31 07:53 +0200 3531 Datatype.ML
-rw-r--r-- 2002-05-31 07:53 +0200 385 Datatype.thy
-rw-r--r-- 2002-05-31 07:53 +0200 12957 Epsilon.thy
-rw-r--r-- 2002-05-31 07:53 +0200 3631 Fin.ML
-rw-r--r-- 2002-05-31 07:53 +0200 85 Fin.thy
-rw-r--r-- 2002-05-31 07:53 +0200 6229 Finite.ML
-rw-r--r-- 2002-05-31 07:53 +0200 938 Finite.thy
-rw-r--r-- 2002-05-31 07:53 +0200 9677 Fixedpt.ML
-rw-r--r-- 2002-05-31 07:53 +0200 569 Fixedpt.thy
-rw-r--r-- 2002-05-31 07:53 +0200 3214 Inductive.ML
-rw-r--r-- 2002-05-31 07:53 +0200 612 Inductive.thy
-rw-r--r-- 2002-05-31 07:53 +0200 3912 InfDatatype.thy
-rw-r--r-- 2002-05-31 07:53 +0200 4030 IsaMakefile
-rw-r--r-- 2002-05-31 07:53 +0200 348 Let.ML
-rw-r--r-- 2002-05-31 07:53 +0200 775 Let.thy
-rw-r--r-- 2002-05-31 07:53 +0200 37788 List.ML
-rw-r--r-- 2002-05-31 07:53 +0200 3391 List.thy
-rw-r--r-- 2002-05-31 07:53 +0200 11464 ListFn.ML
-rw-r--r-- 2002-05-31 07:53 +0200 1607 ListFn.thy
-rw-r--r-- 2002-05-31 07:53 +0200 134 Main.ML
-rw-r--r-- 2002-05-31 07:53 +0200 3384 Main.thy
-rw-r--r-- 2002-05-31 07:53 +0200 3527 Main_ZFC.ML
-rw-r--r-- 2002-05-31 07:53 +0200 43 Main_ZFC.thy
-rw-r--r-- 2002-05-31 07:53 +0200 8975 Nat.thy
-rw-r--r-- 2002-05-31 07:53 +0200 17373 Ord.ML
-rw-r--r-- 2002-05-31 07:53 +0200 737 Ord.thy
-rw-r--r-- 2002-05-31 07:53 +0200 6182 OrdQuant.thy
-rw-r--r-- 2002-05-31 07:53 +0200 24035 Order.thy
-rw-r--r-- 2002-05-31 07:53 +0200 15766 OrderArith.thy
-rw-r--r-- 2002-05-31 07:53 +0200 35827 OrderType.thy
-rw-r--r-- 2002-05-31 07:53 +0200 24980 Ordinal.thy
-rw-r--r-- 2002-05-31 07:53 +0200 4784 Pair.ML
-rw-r--r-- 2002-05-31 07:53 +0200 59 Pair.thy
-rw-r--r-- 2002-05-31 07:53 +0200 18545 Perm.thy
-rw-r--r-- 2002-05-31 07:53 +0200 7906 QPair.ML
-rw-r--r-- 2002-05-31 07:53 +0200 1667 QPair.thy
-rw-r--r-- 2002-05-31 07:53 +0200 6241 QUniv.ML
-rw-r--r-- 2002-05-31 07:53 +0200 561 QUniv.thy
-rw-r--r-- 2002-05-31 07:53 +0200 2389 README.html
-rw-r--r-- 2002-05-31 07:53 +0200 669 ROOT.ML
-rw-r--r-- 2002-05-31 07:53 +0200 1328 Rel.ML
-rw-r--r-- 2002-05-31 07:53 +0200 957 Rel.thy
-rw-r--r-- 2002-05-31 07:53 +0200 4787 Sum.ML
-rw-r--r-- 2002-05-31 07:53 +0200 776 Sum.thy
-rw-r--r-- 2002-05-31 07:53 +0200 8900 Trancl.ML
-rw-r--r-- 2002-05-31 07:53 +0200 514 Trancl.thy
-rw-r--r-- 2002-05-31 07:53 +0200 27728 Univ.thy
-rw-r--r-- 2002-05-31 07:53 +0200 1839 Update.thy
-rw-r--r-- 2002-05-31 07:53 +0200 12225 WF.thy
-rw-r--r-- 2002-05-31 07:53 +0200 14039 ZF.ML
-rw-r--r-- 2002-05-31 07:53 +0200 9863 ZF.thy
-rw-r--r-- 2002-05-31 07:53 +0200 13673 Zorn.thy
-rw-r--r-- 2002-05-31 07:53 +0200 1676 Zorn0.ML
-rw-r--r-- 2002-05-31 07:53 +0200 850 Zorn0.thy
-rw-r--r-- 2002-05-31 07:53 +0200 12291 arith.ML
-rw-r--r-- 2002-05-31 07:53 +0200 878 arith.thy
-rw-r--r-- 2002-05-31 07:53 +0200 8905 arith_data.ML
-rw-r--r-- 2002-05-31 07:53 +0200 4239 bool.ML
-rw-r--r-- 2002-05-31 07:53 +0200 767 bool.thy
-rw-r--r-- 2002-05-31 07:53 +0200 1769 co-inductive.ML
-rw-r--r-- 2002-05-31 07:53 +0200 1762 coinductive.ML
-rw-r--r-- 2002-05-31 07:53 +0200 84 coinductive.thy
-rw-r--r-- 2002-05-31 07:53 +0200 2033 datatype.ML
-rw-r--r-- 2002-05-31 07:53 +0200 194 datatype.thy
-rw-r--r-- 2002-05-31 07:53 +0200 9962 epsilon.ML
-rw-r--r-- 2002-05-31 07:53 +0200 523 epsilon.thy
-rw-r--r-- 2002-05-31 07:53 +0200 27072 equalities.thy
-rw-r--r-- 2002-05-31 07:53 +0200 3482 fin.ML
-rw-r--r-- 2002-05-31 07:53 +0200 115 fin.thy
-rw-r--r-- 2002-05-31 07:53 +0200 11068 fixedpt.ML
-rw-r--r-- 2002-05-31 07:53 +0200 571 fixedpt.thy
-rw-r--r-- 2002-05-31 07:53 +0200 15339 func.thy
-rw-r--r-- 2002-05-31 07:53 +0200 5337 ind-syntax.ML
-rw-r--r-- 2002-05-31 07:53 +0200 6475 ind_syntax.ML
-rw-r--r-- 2002-05-31 07:53 +0200 7275 inductive.ML
-rw-r--r-- 2002-05-31 07:53 +0200 66 inductive.thy
-rw-r--r-- 2002-05-31 07:53 +0200 10794 intr-elim.ML
-rw-r--r-- 2002-05-31 07:53 +0200 2411 list.ML
-rw-r--r-- 2002-05-31 07:53 +0200 83 list.thy
-rw-r--r-- 2002-05-31 07:53 +0200 11464 listfn.ML
-rw-r--r-- 2002-05-31 07:53 +0200 1607 listfn.thy
-rw-r--r-- 2002-05-31 07:53 +0200 5138 mono.ML
-rw-r--r-- 2002-05-31 07:53 +0200 27 mono.thy
-rw-r--r-- 2002-05-31 07:53 +0200 6543 nat.ML
-rw-r--r-- 2002-05-31 07:53 +0200 629 nat.thy
-rw-r--r-- 2002-05-31 07:53 +0200 17373 ord.ML
-rw-r--r-- 2002-05-31 07:53 +0200 737 ord.thy
-rw-r--r-- 2002-05-31 07:53 +0200 4561 pair.ML
-rw-r--r-- 2002-05-31 07:53 +0200 47 pair.thy
-rw-r--r-- 2002-05-31 07:53 +0200 15282 perm.ML
-rw-r--r-- 2002-05-31 07:53 +0200 1066 perm.thy
-rw-r--r-- 2002-05-31 07:53 +0200 9009 qpair.ML
-rw-r--r-- 2002-05-31 07:53 +0200 1613 qpair.thy
-rw-r--r-- 2002-05-31 07:53 +0200 7679 quniv.ML
-rw-r--r-- 2002-05-31 07:53 +0200 357 quniv.thy
-rw-r--r-- 2002-05-31 07:53 +0200 8888 simpdata.ML
-rw-r--r-- 2002-05-31 07:53 +0200 4801 subset.ML
-rw-r--r-- 2002-05-31 07:53 +0200 58 subset.thy
-rw-r--r-- 2002-05-31 07:53 +0200 4635 sum.ML
-rw-r--r-- 2002-05-31 07:53 +0200 744 sum.thy
-rw-r--r-- 2002-05-31 07:53 +0200 6449 thy_syntax.ML
-rw-r--r-- 2002-05-31 07:53 +0200 6800 trancl.ML
-rw-r--r-- 2002-05-31 07:53 +0200 644 trancl.thy
-rw-r--r-- 2002-05-31 07:53 +0200 20259 univ.ML
-rw-r--r-- 2002-05-31 07:53 +0200 927 univ.thy
-rw-r--r-- 2002-05-31 07:53 +0200 10000 upair.ML
-rw-r--r-- 2002-05-31 07:53 +0200 287 upair.thy
-rw-r--r-- 2002-05-31 07:53 +0200 8775 wf.ML
-rw-r--r-- 2002-05-31 07:53 +0200 852 wf.thy
-rw-r--r-- 2002-05-31 07:53 +0200 14167 zf.ML
-rw-r--r-- 2002-05-31 07:53 +0200 7517 zf.thy