Commit 2022-11-14 20:37 3055f901

feat: abel_nf, abel tactic (#555) This is basically a copy-paste job from ring_nf. It adds the analogous things for abel:

• abel1 solves abelian group equalities
• abel_nf rewrites abelian group equalities in hyps or target to a normal form, including recursively inside atoms
• abel_nf is also a conv tactic that does the same thing
• abel calls abel1 and then abel_nf with a trace message
• abel is also a conv tactic that solves equalities by rewriting them to True