diff options
| author | Cyril Cohen | 2018-09-13 13:27:38 +0200 |
|---|---|---|
| committer | Cyril Cohen | 2018-09-13 16:56:37 +0200 |
| commit | 8d8432614e3849ff35f03f098b1a17b4ce41651a (patch) | |
| tree | d30604c961b983116fdc6818c178a08fb7578c6a /ChangeLog | |
| parent | 278b9af169ce8bbac59a96f5f7136dc313b7474a (diff) | |
Small scale tool for proving "the following are equivalent"
Tool to prove only P0 -> P1 -> ... -> Pn -> P0
but use any implication Pi -> Pj
Diffstat (limited to 'ChangeLog')
| -rw-r--r-- | ChangeLog | 5 |
1 files changed, 5 insertions, 0 deletions
@@ -2,6 +2,11 @@ * Added companion matrix of a polynomial `companionmx p` and the theorems: companionmxK, map_mx_companion and companion_map_poly + * Added all_iff, "the following are all equivalent" + with notation [<-> P0; P1; ..; Pn] and theorems + `all_iffLR` and coercion `all_iffP` (see header for doc) + proved by circular implication P0 -> P1 -> ... -> Pn -> P0 + 24/04/2018 - compatibility with Coq 8.8 and several small fixes - version 1.7 * Added compatibility with Coq 8.8 and lost compatibility with |