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-- |
2011-06-17 14:31 +0200 |
1930 |
AC.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2011-06-17 14:31 +0200 |
16573 |
Arith.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2011-06-17 14:31 +0200 |
18320 |
ArithSimp.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2011-06-17 14:31 +0200 |
17220 |
Bin.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2011-06-17 14:31 +0200 |
5532 |
Bool.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2011-06-17 14:31 +0200 |
39399 |
Cardinal.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2011-06-17 14:31 +0200 |
35757 |
CardinalArith.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2011-06-17 14:31 +0200 |
6904 |
Cardinal_AC.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2011-06-17 14:31 +0200 |
3771 |
Datatype_ZF.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2011-06-17 14:31 +0200 |
14192 |
Epsilon.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2011-06-17 14:31 +0200 |
7511 |
EquivClass.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2011-06-17 14:31 +0200 |
6169 |
Finite.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2011-06-17 14:31 +0200 |
9085 |
Fixedpt.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2011-06-17 14:31 +0200 |
3637 |
Inductive_ZF.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2011-06-17 14:31 +0200 |
3912 |
InfDatatype.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2011-06-17 14:31 +0200 |
2553 |
IntArith.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2011-06-17 14:31 +0200 |
59098 |
IntDiv_ZF.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2011-06-17 14:31 +0200 |
29416 |
Int_ZF.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2011-06-17 14:31 +0200 |
4699 |
IsaMakefile
|
file |
revisions |
annotate
|
-rw-r--r-- |
2011-06-17 14:31 +0200 |
36289 |
List_ZF.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2011-06-17 14:31 +0200 |
40 |
Main.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2011-06-17 14:31 +0200 |
2286 |
Main_ZF.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2011-06-17 14:31 +0200 |
55 |
Main_ZFC.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2011-06-17 14:31 +0200 |
8415 |
Nat_ZF.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2011-06-17 14:31 +0200 |
11832 |
OrdQuant.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2011-06-17 14:31 +0200 |
23402 |
Order.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2011-06-17 14:31 +0200 |
18327 |
OrderArith.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2011-06-17 14:31 +0200 |
34977 |
OrderType.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2011-06-17 14:31 +0200 |
21295 |
Ordinal.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2011-06-17 14:31 +0200 |
16131 |
Perm.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2011-06-17 14:31 +0200 |
8077 |
QPair.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2011-06-17 14:31 +0200 |
6233 |
QUniv.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2011-06-17 14:31 +0200 |
2577 |
README.html
|
file |
revisions |
annotate
|
-rw-r--r-- |
2011-06-17 14:31 +0200 |
330 |
ROOT.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2011-06-17 14:31 +0200 |
4588 |
Sum.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2011-06-17 14:31 +0200 |
11078 |
Trancl.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2011-06-17 14:31 +0200 |
24290 |
Univ.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2011-06-17 14:31 +0200 |
11640 |
WF.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2011-06-17 14:31 +0200 |
22238 |
ZF.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2011-06-17 14:31 +0200 |
17859 |
Zorn.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2011-06-17 14:31 +0200 |
9315 |
arith_data.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2011-06-17 14:31 +0200 |
26783 |
equalities.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2011-06-17 14:31 +0200 |
18251 |
func.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2011-06-17 14:31 +0200 |
4539 |
ind_syntax.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2011-06-17 14:31 +0200 |
13758 |
int_arith.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2011-06-17 14:31 +0200 |
4951 |
pair.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2011-06-17 14:31 +0200 |
1629 |
simpdata.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2011-06-17 14:31 +0200 |
14752 |
upair.thy
|
file |
revisions |
annotate
|