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

generalize some lemmas

generalize lemma convex_cone_hull

rename subset_{interior,closure} to {interior,closure}_mono; remove some legacy theorem names;

simplify many proofs about subspace and span; reorder premises in rule span_induct;

remove duplicate simp declaration

simplify definition of 'interior'; add lemmas interiorI and interiorE; change lemmas interior_unique and closure_unique to rule_format; tidy some proofs;

add lemma closure_union; simplify some proofs;

minimize imports

move everything related to 'norm' method into new theory file Norm_Arith.thy

remove unused lemmas dimensionI, dimension_eq

move geometric progression lemmas from Linear_Algebra.thy to Integration.thy where they are used

merge

FSet: Explicit proof without mem_def

merged

added lemma

added a component in generated file names reflecting whether the minimizer is used -- needed for evaluation to keep these files separated from the main problem files

comment

disable TFF for Vampire 1.8 until they've fixed the soundness issues and it's back on SystemOnTPTP

improve completeness of polymorphic encodings

mangle tag bound declarations properly

fixed inverted logic and improve precision when handling monotonic types in polymorphic encodings

make sure that if slicing is disabled, a non-SOS slice is chosen

honor TFF Implicit

make polymorphic encodings more complete

make default unsound mode less unsound

make TFF output less explicit where possible

use more appropriate encoding for Z3 TPTP, as confirmed by evaluation

added one more known Z3 failure

added config options to control two aspects of the translation, for evaluation purposes

added choice operator output for Satallax

rationalized option names -- mono becomes raw_mono and mangled becomes mono

handle nonmangled monomorphich the same way as mangled monomorphic when it comes to helper -- otherwise we can end up generating too tight type guards

avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics

fixed bang encoding detection of which types to encode

lemma Compl_insert: "- insert x A = (-A) - {x}"

avoid variable clashes by properly incrementing indices

improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization

include chained facts for minimizer, otherwise it won't work

remove Vampire imconplete proof detection -- the bug it was trying to work around has been fixed in version 1.8, and the check is too sensitive anyway

back to tradition Scratch.thy default -- execution wrt. perspective overcomes the main problems of 226563829580;

tuned Session.edit_node: update_perspective based on last_exec_offset;

tuned signature -- iterate subsumes both fold and get_first;

further clarification of Document.updated, based on last_common and after_entry; tuned;