/src/ZF/
drwxr-xr-x [up]
drwxr-xr-x AC
drwxr-xr-x Coind
drwxr-xr-x Constructible
drwxr-xr-x IMP
drwxr-xr-x Induct
drwxr-xr-x Resid
drwxr-xr-x Tools
drwxr-xr-x UNITY
drwxr-xr-x document
drwxr-xr-x ex
-rw-r--r-- 2012-03-15 17:38 +0000 1975 AC.thy
-rw-r--r-- 2012-03-15 17:38 +0000 16749 Arith.thy
-rw-r--r-- 2012-03-15 17:38 +0000 19010 ArithSimp.thy
-rw-r--r-- 2012-03-15 17:38 +0000 17761 Bin.thy
-rw-r--r-- 2012-03-15 17:38 +0000 4266 Bool.thy
-rw-r--r-- 2012-03-15 17:38 +0000 37547 Cardinal.thy
-rw-r--r-- 2012-03-15 17:38 +0000 35183 CardinalArith.thy
-rw-r--r-- 2012-03-15 17:38 +0000 7648 Cardinal_AC.thy
-rw-r--r-- 2012-03-15 17:38 +0000 3771 Datatype_ZF.thy
-rw-r--r-- 2012-03-15 17:38 +0000 12319 Epsilon.thy
-rw-r--r-- 2012-03-15 17:38 +0000 7946 EquivClass.thy
-rw-r--r-- 2012-03-15 17:38 +0000 6651 Finite.thy
-rw-r--r-- 2012-03-15 17:38 +0000 9737 Fixedpt.thy
-rw-r--r-- 2012-03-15 17:38 +0000 3655 Inductive_ZF.thy
-rw-r--r-- 2012-03-15 17:38 +0000 3980 InfDatatype.thy
-rw-r--r-- 2012-03-15 17:38 +0000 2684 IntArith.thy
-rw-r--r-- 2012-03-15 17:38 +0000 59615 IntDiv_ZF.thy
-rw-r--r-- 2012-03-15 17:38 +0000 30259 Int_ZF.thy
-rw-r--r-- 2012-03-15 17:38 +0000 4675 IsaMakefile
-rw-r--r-- 2012-03-15 17:38 +0000 37980 List_ZF.thy
-rw-r--r-- 2012-03-15 17:38 +0000 40 Main.thy
-rw-r--r-- 2012-03-15 17:38 +0000 2278 Main_ZF.thy
-rw-r--r-- 2012-03-15 17:38 +0000 55 Main_ZFC.thy
-rw-r--r-- 2012-03-15 17:38 +0000 8827 Nat_ZF.thy
-rw-r--r-- 2012-03-15 17:38 +0000 12522 OrdQuant.thy
-rw-r--r-- 2012-03-15 17:38 +0000 24479 Order.thy
-rw-r--r-- 2012-03-15 17:38 +0000 18823 OrderArith.thy
-rw-r--r-- 2012-03-15 17:38 +0000 35706 OrderType.thy
-rw-r--r-- 2012-03-15 17:38 +0000 22838 Ordinal.thy
-rw-r--r-- 2012-03-15 17:38 +0000 17104 Perm.thy
-rw-r--r-- 2012-03-15 17:38 +0000 8555 QPair.thy
-rw-r--r-- 2012-03-15 17:38 +0000 6449 QUniv.thy
-rw-r--r-- 2012-03-15 17:38 +0000 2577 README.html
-rw-r--r-- 2012-03-15 17:38 +0000 330 ROOT.ML
-rw-r--r-- 2012-03-15 17:38 +0000 4977 Sum.thy
-rw-r--r-- 2012-03-15 17:38 +0000 11374 Trancl.thy
-rw-r--r-- 2012-03-15 17:38 +0000 24825 Univ.thy
-rw-r--r-- 2012-03-15 17:38 +0000 12422 WF.thy
-rw-r--r-- 2012-03-15 17:38 +0000 22597 ZF.thy
-rw-r--r-- 2012-03-15 17:38 +0000 18449 Zorn.thy
-rw-r--r-- 2012-03-15 17:38 +0000 9320 arith_data.ML
-rw-r--r-- 2012-03-15 17:38 +0000 28726 equalities.thy
-rw-r--r-- 2012-03-15 17:38 +0000 19680 func.thy
-rw-r--r-- 2012-03-15 17:38 +0000 4538 ind_syntax.ML
-rw-r--r-- 2012-03-15 17:38 +0000 13758 int_arith.ML
-rw-r--r-- 2012-03-15 17:38 +0000 5357 pair.thy
-rw-r--r-- 2012-03-15 17:38 +0000 1629 simpdata.ML
-rw-r--r-- 2012-03-15 17:38 +0000 17846 upair.thy