v1.0.13
What's Changed
- disable Alectryon by @h0nzZik in #329
- Evaluation of proof mode by @berpeti in #330
mlDestructImp
andmlRevert
by @berpeti in #331- The general deduction theorem from the 2019 paper by @h0nzZik in #332
- mlDeduct "H": a wrapper tactic for Deduction theorem by @h0nzZik in #333
- remove wflexprod.v by @h0nzZik in #334
- Example: mlRewrite under binders by @h0nzZik in #335
- Equality tactics:
mlReflexivity
,mlSymmetry
by @berpeti in #336 - Move and mark
Unification.v
as ongoing work by @berpeti in #337
Full Changelog: v1.0.12...v1.0.13