clarified define_command: store name as structural information;

amended last_common, if that happens to the very last entry (important to load HOL/Auth, for example); clarified touch_node: reset result explicitly;

more redable Document.Node.toString;

sort wrt. theory name;

modernized theory name;

repaired benchmarks;

merged

tuning

always measure time for ATPs -- auto minimization relies on it

added two lemmas about "distinct" to help Sledgehammer

make "sound" sound and "unsound" more sound, based on evaluation

HOL/Import: observe distinction between sets and predicates (where possible)

simplify/generalize some proofs

generalize lemma isCont_vec_nth

convert proof to Isar-style

remove redundant lemma card_enum

move lemmas from Topology_Euclidean_Space to Euclidean_Space

convert to Isar-style proof

make SML/NJ happy

more tuning

more tuning

tuning

avoid relying on dubious TFF1 feature

killed FIXME (the ATP exporter outputs TPTP FOF, which is first-order)

fixed explicit declaration of TFF1 types

adding list_size_append (thanks to Rene Thiemann)

strengthening list_size_pointwise (thanks to Rene Thiemann)

more flexible sorting; tuned display;

tuned signature;

more abstract Document.Node.Name; tuned signature;

more careful treatment of interrupts, to retain them within forked/joined boundary of command transactions;

crude display of node status; tuned signature;

explicit cancel_execution before queueing new edits -- potential performance improvement for machines with few cores;

explicit running_color; stronger colors for overview, more transparent colors for status within text;

tuned join_commands: avoid traversing cumulative table;

some support for theory status overview;

tuned Commands_Changed: cover nodes as well;

maintain name of *the* enclosing node as part of command -- avoid full document traversal;

improved auto loading: selectable file list;

tuned document;

tuned import; discontinued obsolete Sorting.thy (cf. 4d57f872dc2c);

tuned document;

tuned color for Mac OS X (very light color profile?);

tuned document;

merged;

fixed just introduced silly bug

"simple" was renamed "mono_simple" and there's now "poly_simple" as well -- but they are not needed here since for Metis they amount to the same as guards

tuning

cleaner "pff" dummy TFF0 prover

generate properly typed TFF1 (PFF) problems in the presence of type class predicates

added type abstractions (for declaring polymorphic constants) to TFF syntax

implement more of the polymorphic simply typed format TFF(1)

flip logic of boolean option so it's off by default

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

tuned

split timeout among ATPs in and add Metis to the mix as backup

more portable cp options, e.g. for non-GNU version on Mac OS X Leopard;

tuned positions of ambiguity messages -- less intrusive in IDE view;

tuned

merged

avoid loading List_Cset and Dlist_Cet at the same time

corrected slip

Cset, Dlist_Cset, List_Cset: restructured

Cset, Dlist_Cset, List_Cset: restructured

adapted to changes in Cset.thy

adapted to changes in Cset.thy

separating predicates and sets syntactically

merged

avoid intermixing set and predicates; dropped lemmas mem_rsp and mem_prs (now in Quotient_Set.thy)

updated generated files

merged

updated generated files

explicit markup for legacy warnings;

updated generated files;

less aggressive warning icon;

tuned colors;

transparent foreground color for quoted entities;

more precise treatment of nodes that are fully required for partially visible ones;

de-assigned commands also count as changed;

beef up sledgehammer_tac in Mirabelle some more

merged

change default for generation of tag idempotence and tag argument equations

merged

NEWS entry for setsum_norm ~> norm_setsum

make HOL-Probability respect set/pred distinction

merged

use rename_tac to make proof script more robust (with separate set type, 'clarify' yields different variable names)

merged

generalize and simplify proof of continuous_within_sequentially

add lemma sequentially_imp_eventually_within; rename LIMSEQ_SEQ_conv2_lemma to sequentially_imp_eventually_at;

replace some continuous_on lemmas with more general versions

remove legacy theorem Lim_inner

arrange everything related to ordered_euclidean_space class together

generalize and shorten proof of basis_orthogonal

remove dot_lsum and dot_rsum in favor of inner_setsum_{left,right}

merged

generalize lemma finite_imp_compact_convex_hull and related lemmas