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-- |
2008-12-17 17:53 +0100 |
1952 |
AC.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2008-12-17 17:53 +0100 |
16595 |
Arith.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2008-12-17 17:53 +0100 |
18341 |
ArithSimp.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2008-12-17 17:53 +0100 |
17153 |
Bin.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2008-12-17 17:53 +0100 |
5517 |
Bool.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2008-12-17 17:53 +0100 |
39286 |
Cardinal.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2008-12-17 17:53 +0100 |
35657 |
CardinalArith.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2008-12-17 17:53 +0100 |
6923 |
Cardinal_AC.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2008-12-17 17:53 +0100 |
3819 |
Datatype_ZF.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2008-12-17 17:53 +0100 |
14164 |
Epsilon.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2008-12-17 17:53 +0100 |
7533 |
EquivClass.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2008-12-17 17:53 +0100 |
6182 |
Finite.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2008-12-17 17:53 +0100 |
9106 |
Fixedpt.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2008-12-17 17:53 +0100 |
3658 |
Inductive_ZF.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2008-12-17 17:53 +0100 |
3926 |
InfDatatype.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2008-12-17 17:53 +0100 |
2553 |
IntArith.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2008-12-17 17:53 +0100 |
58921 |
IntDiv_ZF.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2008-12-17 17:53 +0100 |
29421 |
Int_ZF.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2008-12-17 17:53 +0100 |
4648 |
IsaMakefile
|
file |
revisions |
annotate
|
-rw-r--r-- |
2008-12-17 17:53 +0100 |
36336 |
List_ZF.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2008-12-17 17:53 +0100 |
52 |
Main.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2008-12-17 17:53 +0100 |
2292 |
Main_ZF.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2008-12-17 17:53 +0100 |
67 |
Main_ZFC.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2008-12-17 17:53 +0100 |
8427 |
Nat_ZF.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2008-12-17 17:53 +0100 |
11985 |
OrdQuant.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2008-12-17 17:53 +0100 |
23332 |
Order.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2008-12-17 17:53 +0100 |
18349 |
OrderArith.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2008-12-17 17:53 +0100 |
34985 |
OrderType.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2008-12-17 17:53 +0100 |
21317 |
Ordinal.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2008-12-17 17:53 +0100 |
15857 |
Perm.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2008-12-17 17:53 +0100 |
8102 |
QPair.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2008-12-17 17:53 +0100 |
6235 |
QUniv.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2008-12-17 17:53 +0100 |
2592 |
README.html
|
file |
revisions |
annotate
|
-rw-r--r-- |
2008-12-17 17:53 +0100 |
368 |
ROOT.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2008-12-17 17:53 +0100 |
4598 |
Sum.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2008-12-17 17:53 +0100 |
11100 |
Trancl.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2008-12-17 17:53 +0100 |
24263 |
Univ.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2008-12-17 17:53 +0100 |
11661 |
WF.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2008-12-17 17:53 +0100 |
22162 |
ZF.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2008-12-17 17:53 +0100 |
17790 |
Zorn.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2008-12-17 17:53 +0100 |
9152 |
arith_data.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2008-12-17 17:53 +0100 |
26830 |
equalities.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2008-12-17 17:53 +0100 |
18266 |
func.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2008-12-17 17:53 +0100 |
4568 |
ind_syntax.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2008-12-17 17:53 +0100 |
13235 |
int_arith.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2008-12-17 17:53 +0100 |
4199 |
pair.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2008-12-17 17:53 +0100 |
2457 |
simpdata.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2008-12-17 17:53 +0100 |
14766 |
upair.thy
|
file |
revisions |
annotate
|