Mode | Name | Size | |
---|---|---|---|
-rw-r--r-- | .cvsignore | 5 | logplain |
-rw-r--r-- | Disjoint_Union.v | 1539 | logplain |
-rw-r--r-- | Inclusion.v | 1001 | logplain |
-rw-r--r-- | Inverse_Image.v | 1677 | logplain |
-rw-r--r-- | Lexicographic_Exponentiation.v | 9403 | logplain |
-rw-r--r-- | Lexicographic_Product.v | 4514 | logplain |
-rw-r--r-- | Transitive_Closure.v | 1425 | logplain |
-rw-r--r-- | Union.v | 2206 | logplain |
-rw-r--r-- | Well_Ordering.v | 1809 | logplain |
-rw-r--r-- | Wellfounded.v | 792 | logplain |
-rwxr-xr-x | intro.tex | 127 | logplain |