NaturalDeduction: allow multi-rule implementations for SequentExpansion and TreeStruc...
[coq-hetmet.git] / src / NaturalDeduction.v
2011-03-28 Adam MegaczNaturalDeduction: allow multi-rule implementations...
2011-03-26 Adam Megaczfinish definitions for SequentCalculus, CutRule, Sequen...
2011-03-26 Adam Megaczre-arrange NaturalDeduction
2011-03-26 Adam Megaczfix proof that Judgments(L) is Cartesian
2011-03-25 Adam Megaczadd n-ary form of nd_weak
2011-03-25 Adam Megaczadd ndr_void_proofs_irrelevant
2011-03-22 Adam Megaczproofs that Types/Judgments form an enrichment
2011-03-19 Adam Megaczadd closedNDtoNormalND to NaturalDeduction
2011-03-07 Adam Megaczcleaned up lots of FIXMEs in ProofToLatex
2011-03-02 Adam MegaczInitial checkin of Coq-in-GHC code