]> matita.cs.unibo.it Git - helm.git/tree - helm/software/matita/dama/
snapshot with more duality, almost where we left without duality
[helm.git] / helm / software / matita / dama /
drwxr-xr-x   ..
-rw-r--r-- 147 Makefile
-rw-r--r-- 6401 Q_is_orded_divisble_group.ma
-rw-r--r-- 125 TODO
drwxr-xr-x - attic
drwxr-xr-x - classical_pointfree
drwxr-xr-x - classical_pointwise
-rw-r--r-- 2236 constructive_connectives.ma
-rw-r--r-- 2253 constructive_higher_order_relations.ma
drwxr-xr-x - constructive_pointfree
-rw-r--r-- 1758 depends
-rw-r--r-- 3812 divisible_group.ma
drwxr-xr-x - doc
-rw-r--r-- 10395 excess.ma
-rw-r--r-- 8465 group.ma
-rw-r--r-- 3536 infsup.ma
-rw-r--r-- 12500 lattice.ma
-rw-r--r-- 2678 limit.ma
-rw-r--r-- 4878 metric_lattice.ma
-rw-r--r-- 2530 metric_space.ma
-rw-r--r-- 3086 ordered_divisible_group.ma
-rw-r--r-- 11050 ordered_group.ma
-rw-r--r-- 3208 premetric_lattice.ma
-rw-r--r-- 13276 prevalued_lattice.ma
-rw-r--r-- 21 root
-rw-r--r-- 3965 sandwich.ma
-rw-r--r-- 2304 sandwich_corollary.ma
-rw-r--r-- 1215 sequence.ma
-rw-r--r-- 1504 tend.ma