rewr_cconv: ignore premises when tuning conclusion

enable \<hole> syntax for rewrite

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

predicate compiler: ignore Abs_filter and Rep_filter

merged

moved _aux functions from AFP/Collections to AList

merged

replace Filters in NSA by HOL-Filters

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

add cofinite filter

add frequently as dual for eventually

add quantifier syntax for eventually

move filters to their own theory

fix latex in Transcendental

proper site for Cygwin setup;

less ambitious collection of quasi-generic PIDE modules;

tuned;

autorebase.bat.done no longer exists in Cygwin 1.7.35 -- lets hope that its incremental rebasing works for us;

merged

tuned -- avoid ML warnings;

avoid redundant shell process;

clarified language_path markup (again): exactly once *after* static phase, see also 83071f4c8ae6 and c043306d2598;

Restored LIMSEQ_def as legacy binding. [The other changes are whitespace only.]

tuned;

merged

proper Pretty.brk -- redundant spaces do not survive Pretty.text (see also 42b7b76b37b8, e06eabc421e7);

tuned whitespace;

Merge

Complex roots of unity. Better definition of ln for complex numbers. Used [code del] to stop code generation for powr.

Merge