From 01dc8db691f533de49f53dfdd173195336731c2b Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 17 Nov 2011 00:07:33 +0000 Subject: [PATCH] Towards 0.95.1. --- matita/matita/dist/ChangeLog | 4 ++++ matita/matita/dist/TODO | 5 +---- 2 files changed, 5 insertions(+), 4 deletions(-) diff --git a/matita/matita/dist/ChangeLog b/matita/matita/dist/ChangeLog index dca7c2abf..90d654b7f 100644 --- a/matita/matita/dist/ChangeLog +++ b/matita/matita/dist/ChangeLog @@ -3,6 +3,10 @@ * new compact syntax for tactics * improved automation * experimental multi tabbed interface + * John Major equality and the computation version of the K axiom are + now in the standard library + * generation of inversion/destruct principles using either + Leibniz or John Major equalities * several bug fixes 0.5.7 - 15/02/2009 - Pàdoa release diff --git a/matita/matita/dist/TODO b/matita/matita/dist/TODO index 5305382b0..d75c433f3 100644 --- a/matita/matita/dist/TODO +++ b/matita/matita/dist/TODO @@ -2,13 +2,10 @@ TODO: - "ncoercion" statement: - simple syntax - generation of hints to implement the pullback -- principles generation: - - induction/inversions - dependency graphs - queries (on the trie?) - Tactics: - - satuation - - destruct + - saturation - ncut - nclearbody - nletin che prende il tipo -- 2.39.2