isabelle: Changelog

noschinl [Mon, 13 Apr 2015 10:39:49 +0200] rev 60048

rewr_cconv: ignore premises when tuning conclusion

noschinl [Mon, 13 Apr 2015 10:21:35 +0200] rev 60047

enable \<hole> syntax for rewrite

traytel [Mon, 13 Apr 2015 13:03:41 +0200] rev 60046

call Goal.prove only once for a quadratic number of theorems

hoelzl [Mon, 13 Apr 2015 12:15:29 +0200] rev 60045

predicate compiler: ignore Abs_filter and Rep_filter

nipkow [Mon, 13 Apr 2015 12:13:52 +0200] rev 60044

merged

nipkow [Mon, 13 Apr 2015 10:36:06 +0200] rev 60043

moved _aux functions from AFP/Collections to AList

hoelzl [Mon, 13 Apr 2015 00:59:17 +0200] rev 60042

merged

hoelzl [Sun, 12 Apr 2015 11:34:16 +0200] rev 60041

replace Filters in NSA by HOL-Filters

hoelzl [Sun, 12 Apr 2015 11:34:09 +0200] rev 60040

move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter

hoelzl [Sun, 12 Apr 2015 11:33:50 +0200] rev 60039

add cofinite filter

isabelle