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;

tuned signature;

improved Document.edit: more accurate update_start and no_execs; tuned;

refined document state assignment: observe perspective, more explicit assignment message; misc tuning and clarification;

tuned signature -- emphasize traditional read/eval/print terminology, which is still relevant here;

maintain last_execs assignment on Scala side; prefer tables over IDs instead of objects;

propagate information about last command with exec state assignment through document model;

tuned signature;

slightly more abstract Command.Perspective;

slightly more abstract Text.Perspective;

tuned proofs;

tuned syntax -- avoid ambiguities;

more accurate treatment of index syntax constants, for proper entity references in concrete notation (e.g. infix "\<oplus>\<index>");

delete commented-out dead code

merged

change some subsection headings to subsubsection

remove unnecessary lemma card_ge1

move connected_real_lemma to the one place it is used

merged

make sure that all facts are passed to ATP from minimizer

more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"

specify timeout for "sledgehammer_tac"

tuning

Quotient Package: add mem_rsp, mem_prs, tune proofs.

merged

declare euclidean_simps [simp] at the point they are proved; avoid duplicate rule warnings;

merged

merged

avoid warnings

comment out dead code to avoid compiler warnings

legacy theorem names

remove duplicate lemma

fixed "hBOOL" of existential variables, and generate more helpers

don't select facts when using sledgehammer_tac for reconstruction

don't perform a triviality check if the goal is skipped anyway

optional reconstructor

misc tuning and simplification;

tuned pri: prefer purging of canceled execution;

tuned Document.node: maintain "touched" flag to indicate changes in entries etc.;

clarified Document.Node.clear -- retain header (cf. ML version);

clarified norm_header/header_edit -- disallow update of loaded theories;

misc tuning and simplification;

ignore irrelevant timings;

print state only for visible command, to avoid wasting resources for the larger part of the text;

early filtering of unchanged perspective;

more reliable update_perspective handler based on actual text visibility (e.g. on startup or when resizing without scrolling);

update_perspective without actual edits, bypassing the full state assignment protocol; edit_nodes/Perspective: do not touch_descendants here; propagate editor scroll events via update_perspective; misc tuning;

tuned;

handle potentially more approriate BufferUpdate.LOADED event;

special treatment of structure index 1 in Pure, including legacy warning;

compile

added "max_calls" option to get a fixed number of Sledgehammer calls per theory

beef up "sledgehammer_tac" reconstructor

clean up Sledgehammer tactic

fixed document;

tuned signature;

merged

always use TFF if possible

clearer separator in generated file names

exploit TFF format in Z3 used as ATP, and renamed it "z3_tptp"

updated known failures for Z3 3.0 TPTP

updated Z3 docs

avoid TFF format with older Vampire versions

update the Vampire related parts of the documentation

fixed TFF slicing

kindly ask Vampire to output axiom names

added formats to the slice and use TFF for remote Vampire

tuned specifications, syntax and proofs

tuned specifications and syntax

Quotient Package: some infrastructure for lifting inside sets

include all encodings in tests, now that the incompleteness of some encodings has been addressed

change Metis's default settings if type information axioms are generated

we must tag any type whose ground types intersect a nonmonotonic type

prefer the lighter, slightly unsound monotonicity-based encodings for Metis

made reconstruction of type tag equalities "\?x = \?x" reliable

tuning ATP problem output

revert guard logic -- make sure that typing information is generated for existentials

generate tag equations for existential variables

tuning, plus started implementing tag equation generation for existential variables

precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis

clearer terminology

renamed "heavy" to "uniform", based on discussion with Nick Smallbone

removed unused configuration option

added caching for (in)finiteness checks

remove needless typing information

cleaner handling of polymorphic monotonicity inference

started cleaning up polymorphic monotonicity-based encodings, based on discussions with Nick Smallbone

more precise warning

added option to control soundness of encodings more precisely, for evaluation purposes

make sound mode more sound (and clean up code)

reintroduced slightly unsound optimization taken out in 717880e98e6b, but only if "sound" is false

gracefully handle empty SPASS problems