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