drwxr-xr-x |
|
|
[up]
|
|
drwxr-xr-x |
|
|
AC
|
files
|
drwxr-xr-x |
|
|
Coind
|
files
|
drwxr-xr-x |
|
|
IMP
|
files
|
drwxr-xr-x |
|
|
Induct
|
files
|
drwxr-xr-x |
|
|
Integ
|
files
|
drwxr-xr-x |
|
|
Resid
|
files
|
drwxr-xr-x |
|
|
Tools
|
files
|
drwxr-xr-x |
|
|
UNITY
|
files
|
drwxr-xr-x |
|
|
ex
|
files
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
2269 |
AC.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
481 |
AC.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
14373 |
Arith.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
1810 |
Arith.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
19072 |
ArithSimp.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
264 |
ArithSimp.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
3851 |
Bool.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
898 |
Bool.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
28544 |
Cardinal.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
1097 |
Cardinal.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
33209 |
CardinalArith.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
5188 |
CardinalArith.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
6696 |
Cardinal_AC.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
264 |
Cardinal_AC.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
3531 |
Datatype.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
385 |
Datatype.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
10998 |
Epsilon.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
987 |
Epsilon.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
3631 |
Fin.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
85 |
Fin.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
6229 |
Finite.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
938 |
Finite.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
9677 |
Fixedpt.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
567 |
Fixedpt.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
3214 |
Inductive.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
612 |
Inductive.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
4022 |
InfDatatype.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
53 |
InfDatatype.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
4263 |
IsaMakefile
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
348 |
Let.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
775 |
Let.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
9500 |
List.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
1714 |
List.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
11464 |
ListFn.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
1607 |
ListFn.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
134 |
Main.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
2866 |
Main.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
61 |
Main_ZFC.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
43 |
Main_ZFC.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
6885 |
Nat.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
655 |
Nat.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
17373 |
Ord.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
737 |
Ord.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
3444 |
OrdQuant.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
5049 |
OrdQuant.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
21881 |
Order.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
1561 |
Order.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
14478 |
OrderArith.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
1187 |
OrderArith.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
32077 |
OrderType.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
1313 |
OrderType.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
20712 |
Ordinal.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
937 |
Ordinal.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
4784 |
Pair.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
59 |
Pair.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
17190 |
Perm.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
1043 |
Perm.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
7866 |
QPair.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
1667 |
QPair.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
6241 |
QUniv.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
561 |
QUniv.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
2389 |
README.html
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
669 |
ROOT.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
1328 |
Rel.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
955 |
Rel.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
4787 |
Sum.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
776 |
Sum.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
8900 |
Trancl.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
514 |
Trancl.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
23003 |
Univ.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
1152 |
Univ.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
1199 |
Update.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
841 |
Update.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
11710 |
WF.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
1150 |
WF.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
14050 |
ZF.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
9576 |
ZF.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
13194 |
Zorn.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
1427 |
Zorn.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
1676 |
Zorn0.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
850 |
Zorn0.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
12291 |
arith.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
878 |
arith.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
8824 |
arith_data.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
4239 |
bool.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
767 |
bool.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
1769 |
co-inductive.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
1762 |
coinductive.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
84 |
coinductive.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
2033 |
datatype.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
194 |
datatype.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
5414 |
domrange.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
70 |
domrange.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
9962 |
epsilon.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
523 |
epsilon.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
16700 |
equalities.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
67 |
equalities.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
3482 |
fin.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
115 |
fin.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
11068 |
fixedpt.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
571 |
fixedpt.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
13584 |
func.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
73 |
func.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
5337 |
ind-syntax.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
6259 |
ind_syntax.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
7275 |
inductive.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
66 |
inductive.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
10794 |
intr-elim.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
2411 |
list.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
83 |
list.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
11464 |
listfn.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
1607 |
listfn.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
5138 |
mono.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
27 |
mono.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
6543 |
nat.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
629 |
nat.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
17373 |
ord.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
737 |
ord.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
4495 |
pair.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
47 |
pair.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
15282 |
perm.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
1066 |
perm.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
9009 |
qpair.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
1613 |
qpair.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
7679 |
quniv.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
357 |
quniv.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
8516 |
simpdata.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
4801 |
subset.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
58 |
subset.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
4635 |
sum.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
744 |
sum.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
6449 |
thy_syntax.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
6800 |
trancl.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
644 |
trancl.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
20259 |
univ.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
927 |
univ.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
10000 |
upair.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
287 |
upair.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
8775 |
wf.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
852 |
wf.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
14167 |
zf.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2002-01-16 17:53 +0100 |
7517 |
zf.thy
|
file |
revisions |
annotate
|