Tue, 18 Sep 2012 11:42:11 +0200 register induct attributes
blanchet [Tue, 18 Sep 2012 11:42:11 +0200] rev 49437
register induct attributes
Tue, 18 Sep 2012 11:41:04 +0200 further tuned simpset
blanchet [Tue, 18 Sep 2012 11:41:04 +0200] rev 49436
further tuned simpset
Tue, 18 Sep 2012 11:06:25 +0200 bnf_note_all mode for "pre_"-BNFs
traytel [Tue, 18 Sep 2012 11:06:25 +0200] rev 49435
bnf_note_all mode for "pre_"-BNFs
Tue, 18 Sep 2012 09:15:53 +0200 separated registration of BNFs from bnf_def (BNFs are now stored only for bnf_def and (co)data commands)
traytel [Tue, 18 Sep 2012 09:15:53 +0200] rev 49434
separated registration of BNFs from bnf_def (BNFs are now stored only for bnf_def and (co)data commands)
Tue, 18 Sep 2012 03:33:53 +0200 tuned
nipkow [Tue, 18 Sep 2012 03:33:53 +0200] rev 49433
tuned
Tue, 18 Sep 2012 03:24:51 +0200 beautified names
nipkow [Tue, 18 Sep 2012 03:24:51 +0200] rev 49432
beautified names
Tue, 18 Sep 2012 01:55:13 +0200 proved all upper bounds
nipkow [Tue, 18 Sep 2012 01:55:13 +0200] rev 49431
proved all upper bounds
Mon, 17 Sep 2012 21:33:12 +0200 tuned simpset
blanchet [Mon, 17 Sep 2012 21:33:12 +0200] rev 49430
tuned simpset
Mon, 17 Sep 2012 21:13:30 +0200 cleaner way of dealing with the set functions of sums and products
blanchet [Mon, 17 Sep 2012 21:13:30 +0200] rev 49429
cleaner way of dealing with the set functions of sums and products
Mon, 17 Sep 2012 21:13:30 +0200 handle the general case with more than two levels of nesting when discharging induction prem prems
blanchet [Mon, 17 Sep 2012 21:13:30 +0200] rev 49428
handle the general case with more than two levels of nesting when discharging induction prem prems
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 tip