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-- |
1997-09-22 17:37 +0200 |
1825 |
AC.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
342 |
AC.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
19403 |
Arith.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
920 |
Arith.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
3914 |
Bool.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
899 |
Bool.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
28043 |
Cardinal.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
893 |
Cardinal.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
32057 |
CardinalArith.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
1120 |
CardinalArith.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
7446 |
Cardinal_AC.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
264 |
Cardinal_AC.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
2021 |
Datatype.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
381 |
Datatype.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
10599 |
Epsilon.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
802 |
Epsilon.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
8774 |
EquivClass.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
666 |
EquivClass.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
3631 |
Fin.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
85 |
Fin.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
4896 |
Finite.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
766 |
Finite.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
10234 |
Fixedpt.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
566 |
Fixedpt.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
4590 |
Inductive.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
97 |
Inductive.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
4165 |
InfDatatype.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
53 |
InfDatatype.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
2353 |
IsaMakefile
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
346 |
Let.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
759 |
Let.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
13286 |
List.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
1760 |
List.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
11464 |
ListFn.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
1607 |
ListFn.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
6996 |
Nat.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
655 |
Nat.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
17373 |
Ord.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
737 |
Ord.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
3536 |
OrdQuant.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
1065 |
OrdQuant.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
22824 |
Order.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
1488 |
Order.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
15116 |
OrderArith.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
1039 |
OrderArith.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
34855 |
OrderType.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
1132 |
OrderType.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
21974 |
Ordinal.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
936 |
Ordinal.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
4784 |
Pair.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
59 |
Pair.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
18250 |
Perm.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
1051 |
Perm.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
8723 |
QPair.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
1665 |
QPair.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
8084 |
QUniv.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
357 |
QUniv.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
2389 |
README.html
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
1338 |
ROOT.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
1487 |
Rel.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
955 |
Rel.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
5143 |
Sum.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
754 |
Sum.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
6428 |
Trancl.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
514 |
Trancl.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
22174 |
Univ.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
933 |
Univ.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
11308 |
WF.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
1149 |
WF.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
14847 |
ZF.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
9118 |
ZF.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
14610 |
Zorn.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
1541 |
Zorn.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
1676 |
Zorn0.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
850 |
Zorn0.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
10144 |
add_ind_def.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
94 |
add_ind_def.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
12291 |
arith.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
878 |
arith.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
4239 |
bool.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
767 |
bool.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
3451 |
cartprod.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
68 |
cartprod.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
1769 |
co-inductive.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
1762 |
coinductive.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
84 |
coinductive.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
3193 |
constructor.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
70 |
constructor.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
2033 |
datatype.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
194 |
datatype.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
6043 |
domrange.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
73 |
domrange.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
9962 |
epsilon.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
523 |
epsilon.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
13220 |
equalities.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
67 |
equalities.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
3482 |
fin.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
115 |
fin.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
11068 |
fixedpt.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
571 |
fixedpt.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
12714 |
func.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
73 |
func.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
5337 |
ind-syntax.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
5075 |
ind_syntax.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
64 |
ind_syntax.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
9526 |
indrule.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
94 |
indrule.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
7275 |
inductive.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
66 |
inductive.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
10794 |
intr-elim.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
6222 |
intr_elim.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
70 |
intr_elim.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
2411 |
list.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
83 |
list.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
11464 |
listfn.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
1607 |
listfn.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
5528 |
mono.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
75 |
mono.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
6543 |
nat.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
629 |
nat.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
17373 |
ord.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
737 |
ord.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
4928 |
pair.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
58 |
pair.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
15282 |
perm.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
1066 |
perm.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
9009 |
qpair.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
1613 |
qpair.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
7679 |
quniv.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
357 |
quniv.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
3462 |
simpdata.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
78 |
simpdata.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
5180 |
subset.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
59 |
subset.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
4635 |
sum.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
744 |
sum.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
6368 |
thy_syntax.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
6800 |
trancl.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
644 |
trancl.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
1169 |
typechk.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
20259 |
univ.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
927 |
univ.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
10132 |
upair.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
281 |
upair.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
8775 |
wf.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
852 |
wf.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
14167 |
zf.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
1997-09-22 17:37 +0200 |
7517 |
zf.thy
|
file |
revisions |
annotate
|