Wed, 12 Sep 2012 23:18:26 +0200 observe context more carefully when producing "fresh" variables -- for increased chances that method "subst" works in local context (including that of forked proofs);
wenzelm [Wed, 12 Sep 2012 23:18:26 +0200] rev 49340
observe context more carefully when producing "fresh" variables -- for increased chances that method "subst" works in local context (including that of forked proofs);
Wed, 12 Sep 2012 22:00:29 +0200 eliminated some old material that is unused in the visible universe;
wenzelm [Wed, 12 Sep 2012 22:00:29 +0200] rev 49339
eliminated some old material that is unused in the visible universe;
Wed, 12 Sep 2012 17:26:05 +0200 tuning
blanchet [Wed, 12 Sep 2012 17:26:05 +0200] rev 49338
tuning
Wed, 12 Sep 2012 17:26:05 +0200 set up things for (co)induction sugar
blanchet [Wed, 12 Sep 2012 17:26:05 +0200] rev 49337
set up things for (co)induction sugar
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -4 +4 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip