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.;
Sun, 09 Nov 2014 14:08:00 +0100 proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
wenzelm [Sun, 09 Nov 2014 14:08:00 +0100] rev 58956
proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
Sun, 09 Nov 2014 11:05:20 +0100 avoid erule and rotated in IMP
nipkow [Sun, 09 Nov 2014 11:05:20 +0100] rev 58955
avoid erule and rotated in IMP
Sun, 09 Nov 2014 10:03:18 +0100 reverted 1ebf0a1f12a4 after successful re-tuning of simp rules for divisibility
haftmann [Sun, 09 Nov 2014 10:03:18 +0100] rev 58954
reverted 1ebf0a1f12a4 after successful re-tuning of simp rules for divisibility
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 tip