Tue, 11 Nov 2014 10:26:08 +0100 make 'rec_transfer' tactic more robust
desharna [Tue, 11 Nov 2014 10:26:08 +0100] rev 58966
make 'rec_transfer' tactic more robust
Tue, 11 Nov 2014 08:57:46 +0100 add del option to measurable;
Andreas Lochbihler [Tue, 11 Nov 2014 08:57:46 +0100] rev 58965
add del option to measurable; make measurability rules available as dynamic theorem;
Tue, 11 Nov 2014 00:11:11 +0100 merged
wenzelm [Tue, 11 Nov 2014 00:11:11 +0100] rev 58964
merged
Mon, 10 Nov 2014 21:49:48 +0100 proper context for assume_tac (atac remains as fall-back without context);
wenzelm [Mon, 10 Nov 2014 21:49:48 +0100] rev 58963
proper context for assume_tac (atac remains as fall-back without context);
Mon, 10 Nov 2014 15:09:58 +0100 even -> evn because even is now in Main
nipkow [Mon, 10 Nov 2014 15:09:58 +0100] rev 58962
even -> evn because even is now in Main
Mon, 10 Nov 2014 10:29:19 +0100 dropped redundant transfer rules (now proved and registered by datatype and plugins)
traytel [Mon, 10 Nov 2014 10:29:19 +0100] rev 58961
dropped redundant transfer rules (now proved and registered by datatype and plugins)
Sun, 09 Nov 2014 20:49:28 +0100 proper context for typedef;
wenzelm [Sun, 09 Nov 2014 20:49:28 +0100] rev 58960
proper context for typedef;
Sun, 09 Nov 2014 20:41:53 +0100 proper proof context for typedef;
wenzelm [Sun, 09 Nov 2014 20:41:53 +0100] rev 58959
proper proof context for typedef;
Sun, 09 Nov 2014 18:27:43 +0100 proper context;
wenzelm [Sun, 09 Nov 2014 18:27:43 +0100] rev 58958
proper context;
Sun, 09 Nov 2014 17:04:14 +0100 proper context for match_tac etc.;
wenzelm [Sun, 09 Nov 2014 17:04:14 +0100] rev 58957
proper context for match_tac etc.;
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 tip