clean up demo code
[coq-hetmet.git] / src / NaturalDeduction.v
2011-05-23 Adam MegaczNaturalDeduction: add nd_exch
2011-04-30 Adam Megaczclean up hints for NaturalDeduction, split ProgrammingL...
2011-04-25 Adam Megaczremove ClosedSIND (use "SIND []" instead)
2011-04-24 Adam MegaczNaturalDeduction: add nd_swap, nd_prod_split, and some...
2011-04-10 Adam Megaczadd commented-out definitions for analytic proofs and...
2011-04-10 Adam Megaczupdate to new coq-categories, base ND_Relation on inert...
2011-04-04 Adam Megaczupdate to account for coq-categories changes
2011-03-29 Adam Megaczformatting fixes
2011-03-29 Adam Megaczlots of cleanup
2011-03-29 Adam MegaczNaturalDeduction: remove unnecessary scnd_leaf, add...
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