From 8d8432614e3849ff35f03f098b1a17b4ce41651a Mon Sep 17 00:00:00 2001
From: Cyril Cohen
Date: Thu, 13 Sep 2018 13:27:38 +0200
Subject: Small scale tool for proving "the following are equivalent"

Tool to prove only P0 -> P1 -> ... -> Pn -> P0
but use any implication Pi -> Pj
---
 ChangeLog | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'ChangeLog')

diff --git a/ChangeLog b/ChangeLog
index d59a140..d6ea65f 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -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
-- 
cgit v1.2.3