drwxr-xr-x |
|
|
[up]
|
|
drwxr-xr-x |
|
|
AC
|
files
|
drwxr-xr-x |
|
|
Coind
|
files
|
drwxr-xr-x |
|
|
IMP
|
files
|
drwxr-xr-x |
|
|
Resid
|
files
|
drwxr-xr-x |
|
|
ex
|
files
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
1856 |
AC.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
339 |
AC.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
12522 |
Arith.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
877 |
Arith.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
4035 |
Bool.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
853 |
Bool.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
24125 |
Cardinal.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
894 |
Cardinal.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
28356 |
CardinalArith.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
1146 |
CardinalArith.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
7096 |
Cardinal_AC.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
257 |
Cardinal_AC.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
1976 |
Datatype.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
167 |
Datatype.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
9660 |
Epsilon.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
522 |
Epsilon.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
8726 |
EquivClass.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
660 |
EquivClass.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
3631 |
Fin.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
85 |
Fin.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
4802 |
Finite.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
750 |
Finite.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
10201 |
Fixedpt.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
570 |
Fixedpt.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
3595 |
Inductive.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
90 |
Inductive.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
4098 |
InfDatatype.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
53 |
InfDatatype.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
332 |
Let.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
734 |
Let.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
13030 |
List.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
1660 |
List.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
11464 |
ListFn.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
1607 |
ListFn.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
3462 |
Makefile
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
6727 |
Nat.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
632 |
Nat.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
17373 |
Ord.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
737 |
Ord.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
22047 |
Order.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
1359 |
Order.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
15493 |
OrderArith.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
1040 |
OrderArith.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
33904 |
OrderType.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
1136 |
OrderType.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
21830 |
Ordinal.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
848 |
Ordinal.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
4784 |
Pair.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
59 |
Pair.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
18826 |
Perm.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
1065 |
Perm.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
8513 |
QPair.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
1607 |
QPair.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
8001 |
QUniv.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
356 |
QUniv.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
2556 |
README
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
1209 |
ROOT.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
1500 |
Rel.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
944 |
Rel.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
5685 |
Sum.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
743 |
Sum.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
6392 |
Trancl.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
513 |
Trancl.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
21867 |
Univ.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
930 |
Univ.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
11461 |
WF.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
1109 |
WF.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
15157 |
ZF.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
7627 |
ZF.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
14456 |
Zorn.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
1539 |
Zorn.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
1676 |
Zorn0.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
850 |
Zorn0.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
9418 |
add_ind_def.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
81 |
add_ind_def.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
12291 |
arith.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
878 |
arith.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
4239 |
bool.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
767 |
bool.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
1769 |
co-inductive.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
1762 |
coinductive.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
84 |
coinductive.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
2843 |
constructor.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
69 |
constructor.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
2033 |
datatype.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
194 |
datatype.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
6302 |
domrange.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
73 |
domrange.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
9962 |
epsilon.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
523 |
epsilon.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
12068 |
equalities.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
68 |
equalities.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
3482 |
fin.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
115 |
fin.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
11068 |
fixedpt.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
571 |
fixedpt.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
12423 |
func.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
77 |
func.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
5337 |
ind-syntax.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
4797 |
ind_syntax.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
64 |
ind_syntax.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
7238 |
indrule.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
81 |
indrule.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
7275 |
inductive.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
66 |
inductive.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
10794 |
intr-elim.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
6074 |
intr_elim.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
70 |
intr_elim.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
2411 |
list.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
83 |
list.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
11464 |
listfn.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
1607 |
listfn.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
5630 |
mono.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
63 |
mono.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
6543 |
nat.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
629 |
nat.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
17373 |
ord.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
737 |
ord.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
6916 |
pair.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
59 |
pair.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
15282 |
perm.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
1066 |
perm.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
9009 |
qpair.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
1613 |
qpair.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
7679 |
quniv.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
357 |
quniv.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
3001 |
simpdata.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
78 |
simpdata.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
6105 |
subset.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
61 |
subset.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
4635 |
sum.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
744 |
sum.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
6111 |
thy_syntax.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
6800 |
trancl.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
644 |
trancl.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
20259 |
univ.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
927 |
univ.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
10494 |
upair.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
55 |
upair.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
8775 |
wf.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
852 |
wf.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
14167 |
zf.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1995-04-28 11:24 +0200 |
7517 |
zf.thy
|
file |
revisions |
annotate
|