Mode | Name | Size | |
---|---|---|---|
-rw-r--r-- | Berardi.v | 4195 | logplain |
-rw-r--r-- | ChoiceFacts.v | 4557 | logplain |
-rwxr-xr-x | Classical.v | 688 | logplain |
-rw-r--r-- | ClassicalChoice.v | 1274 | logplain |
-rw-r--r-- | ClassicalDescription.v | 2510 | logplain |
-rw-r--r-- | ClassicalFacts.v | 7211 | logplain |
-rwxr-xr-x | Classical_Pred_Set.v | 1774 | logplain |
-rwxr-xr-x | Classical_Pred_Type.v | 1786 | logplain |
-rwxr-xr-x | Classical_Prop.v | 2087 | logplain |
-rwxr-xr-x | Classical_Type.v | 702 | logplain |
-rw-r--r-- | Decidable.v | 1794 | logplain |
-rw-r--r-- | Diaconescu.v | 4055 | logplain |
-rwxr-xr-x | Eqdep.v | 5232 | logplain |
-rw-r--r-- | Eqdep_dec.v | 3665 | logplain |
-rw-r--r-- | Hurkens.v | 2472 | logplain |
-rw-r--r-- | JMeq.v | 1927 | logplain |
-rw-r--r-- | ProofIrrelevance.v | 3793 | logplain |
-rw-r--r-- | RelationalChoice.v | 862 | logplain |