drwxr-xr-x |
|
|
[up]
|
|
drwxr-xr-x |
|
|
AC
|
files
|
drwxr-xr-x |
|
|
Coind
|
files
|
drwxr-xr-x |
|
|
Constructible
|
files
|
drwxr-xr-x |
|
|
IMP
|
files
|
drwxr-xr-x |
|
|
Induct
|
files
|
drwxr-xr-x |
|
|
Resid
|
files
|
drwxr-xr-x |
|
|
Tools
|
files
|
drwxr-xr-x |
|
|
UNITY
|
files
|
drwxr-xr-x |
|
|
document
|
files
|
drwxr-xr-x |
|
|
ex
|
files
|
-rw-r--r-- |
2013-01-14 14:53 +0100 |
1975 |
AC.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2013-01-14 14:53 +0100 |
16749 |
Arith.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2013-01-14 14:53 +0100 |
19019 |
ArithSimp.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2013-01-14 14:53 +0100 |
17732 |
Bin.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2013-01-14 14:53 +0100 |
4266 |
Bool.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2013-01-14 14:53 +0100 |
39805 |
Cardinal.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2013-01-14 14:53 +0100 |
35184 |
CardinalArith.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2013-01-14 14:53 +0100 |
9009 |
Cardinal_AC.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2013-01-14 14:53 +0100 |
3820 |
Datatype_ZF.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2013-01-14 14:53 +0100 |
12319 |
Epsilon.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2013-01-14 14:53 +0100 |
7946 |
EquivClass.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2013-01-14 14:53 +0100 |
6651 |
Finite.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2013-01-14 14:53 +0100 |
9737 |
Fixedpt.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2013-01-14 14:53 +0100 |
3753 |
Inductive_ZF.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2013-01-14 14:53 +0100 |
4736 |
InfDatatype.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2013-01-14 14:53 +0100 |
2666 |
IntArith.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2013-01-14 14:53 +0100 |
59378 |
IntDiv_ZF.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2013-01-14 14:53 +0100 |
30259 |
Int_ZF.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2013-01-14 14:53 +0100 |
37980 |
List_ZF.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2013-01-14 14:53 +0100 |
40 |
Main.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2013-01-14 14:53 +0100 |
2278 |
Main_ZF.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2013-01-14 14:53 +0100 |
55 |
Main_ZFC.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2013-01-14 14:53 +0100 |
8827 |
Nat_ZF.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2013-01-14 14:53 +0100 |
12522 |
OrdQuant.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2013-01-14 14:53 +0100 |
24479 |
Order.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2013-01-14 14:53 +0100 |
18823 |
OrderArith.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2013-01-14 14:53 +0100 |
35706 |
OrderType.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2013-01-14 14:53 +0100 |
22945 |
Ordinal.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2013-01-14 14:53 +0100 |
17227 |
Perm.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2013-01-14 14:53 +0100 |
8555 |
QPair.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2013-01-14 14:53 +0100 |
6449 |
QUniv.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2013-01-14 14:53 +0100 |
2577 |
README.html
|
file |
revisions |
annotate
|
-rw-r--r-- |
2013-01-14 14:53 +0100 |
4833 |
ROOT
|
file |
revisions |
annotate
|
-rw-r--r-- |
2013-01-14 14:53 +0100 |
4977 |
Sum.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2013-01-14 14:53 +0100 |
11374 |
Trancl.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2013-01-14 14:53 +0100 |
24825 |
Univ.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2013-01-14 14:53 +0100 |
12470 |
WF.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2013-01-14 14:53 +0100 |
22538 |
ZF.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2013-01-14 14:53 +0100 |
18449 |
Zorn.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2013-01-14 14:53 +0100 |
9320 |
arith_data.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2013-01-14 14:53 +0100 |
28726 |
equalities.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2013-01-14 14:53 +0100 |
19680 |
func.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2013-01-14 14:53 +0100 |
4538 |
ind_syntax.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2013-01-14 14:53 +0100 |
13758 |
int_arith.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2013-01-14 14:53 +0100 |
5361 |
pair.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2013-01-14 14:53 +0100 |
1629 |
simpdata.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2013-01-14 14:53 +0100 |
17880 |
upair.thy
|
file |
revisions |
annotate
|