2011-03-26 | Adam Megacz | re-arrange NaturalDeduction | blob | commitdiff |
2011-03-26 | Adam Megacz | fix proof that Judgments(L) is Cartesian | blob | commitdiff | diff to current |
2011-03-25 | Adam Megacz | add n-ary form of nd_weak | blob | commitdiff | diff to current |
2011-03-25 | Adam Megacz | add ndr_void_proofs_irrelevant | blob | commitdiff | diff to current |
2011-03-22 | Adam Megacz | proofs that Types/Judgments form an enrichment | blob | commitdiff | diff to current |
2011-03-19 | Adam Megacz | add closedNDtoNormalND to NaturalDeduction | blob | commitdiff | diff to current |
2011-03-07 | Adam Megacz | cleaned up lots of FIXMEs in ProofToLatex | blob | commitdiff | diff to current |
2011-03-02 | Adam Megacz | Initial checkin of Coq-in-GHC code | blob | commitdiff | diff to current |