extended simple types with polymorphism -- the implementation still needs some work though

added dummy PFF prover, for debugging purposes

first step towards polymorphic TFF + changed defaults for Vampire

tuning

removed explicit reliance on Hilbert_Choice.Eps

improved handling of induction rules in Sledgehammer

added generation of induction rules

simplify some proofs

restrict perspective to actual buffer_range, to avoid spurious edits due to faulty last_exec_offset (NB: jEdit screenlines may be silently extended by trailing newline);

tuned signature;

dynamic exec state lookup for implicit position information (e.g. 'definition' without binding);

some support for hyperlinks between different buffers; tuned signature;

tuned colors -- more distance between outdated_color and quoted_color;

do not normalized extra file dependencies for now -- still loaded by prover process;

separate module for jEdit primitives for loading theory files;

merged

Product_Vector.thy: clean up some proofs

actual auto loading of required files; eliminated File_Store in favour of Thy_Load; tuned;

some dialog for auto loading of required files (still inactive);

invoke in Swing thread to make double sure;

move class perfect_space into RealVector.thy; use not_open_singleton as perfect_space class axiom; generalize some lemmas to class perfect_space;

generalize LIM_zero lemmas to arbitrary filters

merged

discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems