/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-08 16:43 +0000 1958 AC.thy
-rw-r--r-- 2012-03-08 16:43 +0000 16749 Arith.thy
-rw-r--r-- 2012-03-08 16:43 +0000 19010 ArithSimp.thy
-rw-r--r-- 2012-03-08 16:43 +0000 17491 Bin.thy
-rw-r--r-- 2012-03-08 16:43 +0000 4266 Bool.thy
-rw-r--r-- 2012-03-08 16:43 +0000 35064 Cardinal.thy
-rw-r--r-- 2012-03-08 16:43 +0000 32644 CardinalArith.thy
-rw-r--r-- 2012-03-08 16:43 +0000 7015 Cardinal_AC.thy
-rw-r--r-- 2012-03-08 16:43 +0000 3771 Datatype_ZF.thy
-rw-r--r-- 2012-03-08 16:43 +0000 12168 Epsilon.thy
-rw-r--r-- 2012-03-08 16:43 +0000 7788 EquivClass.thy
-rw-r--r-- 2012-03-08 16:43 +0000 6432 Finite.thy
-rw-r--r-- 2012-03-08 16:43 +0000 9737 Fixedpt.thy
-rw-r--r-- 2012-03-08 16:43 +0000 3655 Inductive_ZF.thy
-rw-r--r-- 2012-03-08 16:43 +0000 3980 InfDatatype.thy
-rw-r--r-- 2012-03-08 16:43 +0000 2674 IntArith.thy
-rw-r--r-- 2012-03-08 16:43 +0000 59615 IntDiv_ZF.thy
-rw-r--r-- 2012-03-08 16:43 +0000 30193 Int_ZF.thy
-rw-r--r-- 2012-03-08 16:43 +0000 4675 IsaMakefile
-rw-r--r-- 2012-03-08 16:43 +0000 37445 List_ZF.thy
-rw-r--r-- 2012-03-08 16:43 +0000 40 Main.thy
-rw-r--r-- 2012-03-08 16:43 +0000 2294 Main_ZF.thy
-rw-r--r-- 2012-03-08 16:43 +0000 55 Main_ZFC.thy
-rw-r--r-- 2012-03-08 16:43 +0000 8588 Nat_ZF.thy
-rw-r--r-- 2012-03-08 16:43 +0000 12500 OrdQuant.thy
-rw-r--r-- 2012-03-08 16:43 +0000 24127 Order.thy
-rw-r--r-- 2012-03-08 16:43 +0000 18870 OrderArith.thy
-rw-r--r-- 2012-03-08 16:43 +0000 35051 OrderType.thy
-rw-r--r-- 2012-03-08 16:43 +0000 22933 Ordinal.thy
-rw-r--r-- 2012-03-08 16:43 +0000 16525 Perm.thy
-rw-r--r-- 2012-03-08 16:43 +0000 8446 QPair.thy
-rw-r--r-- 2012-03-08 16:43 +0000 6449 QUniv.thy
-rw-r--r-- 2012-03-08 16:43 +0000 2577 README.html
-rw-r--r-- 2012-03-08 16:43 +0000 330 ROOT.ML
-rw-r--r-- 2012-03-08 16:43 +0000 4913 Sum.thy
-rw-r--r-- 2012-03-08 16:43 +0000 11328 Trancl.thy
-rw-r--r-- 2012-03-08 16:43 +0000 24825 Univ.thy
-rw-r--r-- 2012-03-08 16:43 +0000 12261 WF.thy
-rw-r--r-- 2012-03-08 16:43 +0000 22506 ZF.thy
-rw-r--r-- 2012-03-08 16:43 +0000 18449 Zorn.thy
-rw-r--r-- 2012-03-08 16:43 +0000 9320 arith_data.ML
-rw-r--r-- 2012-03-08 16:43 +0000 28726 equalities.thy
-rw-r--r-- 2012-03-08 16:43 +0000 19342 func.thy
-rw-r--r-- 2012-03-08 16:43 +0000 4538 ind_syntax.ML
-rw-r--r-- 2012-03-08 16:43 +0000 13758 int_arith.ML
-rw-r--r-- 2012-03-08 16:43 +0000 5319 pair.thy
-rw-r--r-- 2012-03-08 16:43 +0000 1629 simpdata.ML
-rw-r--r-- 2012-03-08 16:43 +0000 17623 upair.thy