2011-08-25 blanchet 2011-08-25 make default unsound mode less unsound
2011-08-25 blanchet 2011-08-25 make TFF output less explicit where possible
2011-08-25 blanchet 2011-08-25 use more appropriate encoding for Z3 TPTP, as confirmed by evaluation
2011-08-25 blanchet 2011-08-25 added one more known Z3 failure
2011-08-25 blanchet 2011-08-25 added config options to control two aspects of the translation, for evaluation purposes
2011-08-25 nik 2011-08-25 added choice operator output for Satallax
2011-08-25 blanchet 2011-08-25 rationalized option names -- mono becomes raw_mono and mangled becomes mono
2011-08-25 blanchet 2011-08-25 handle nonmangled monomorphich the same way as mangled monomorphic when it comes to helper -- otherwise we can end up generating too tight type guards
2011-08-25 blanchet 2011-08-25 avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
2011-08-25 blanchet 2011-08-25 fixed bang encoding detection of which types to encode
2011-08-25 krauss 2011-08-25 lemma Compl_insert: "- insert x A = (-A) - {x}"
2011-08-25 boehmes 2011-08-25 avoid variable clashes by properly incrementing indices
2011-08-25 boehmes 2011-08-25 improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
2011-08-25 blanchet 2011-08-25 include chained facts for minimizer, otherwise it won't work
2011-08-24 blanchet 2011-08-24 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
2011-08-26 wenzelm 2011-08-26 back to tradition Scratch.thy default -- execution wrt. perspective overcomes the main problems of 226563829580;
2011-08-26 wenzelm 2011-08-26 tuned Session.edit_node: update_perspective based on last_exec_offset;
2011-08-26 wenzelm 2011-08-26 tuned signature -- iterate subsumes both fold and get_first;
2011-08-26 wenzelm 2011-08-26 further clarification of Document.updated, based on last_common and after_entry; tuned;
2011-08-26 wenzelm 2011-08-26 tuned signature;
2011-08-26 wenzelm 2011-08-26 improved Document.edit: more accurate update_start and no_execs; tuned;
2011-08-26 wenzelm 2011-08-26 refined document state assignment: observe perspective, more explicit assignment message; misc tuning and clarification;
2011-08-25 wenzelm 2011-08-25 tuned signature -- emphasize traditional read/eval/print terminology, which is still relevant here;
2011-08-25 wenzelm 2011-08-25 maintain last_execs assignment on Scala side; prefer tables over IDs instead of objects;
2011-08-25 wenzelm 2011-08-25 propagate information about last command with exec state assignment through document model;
2011-08-25 wenzelm 2011-08-25 tuned signature;
2011-08-25 wenzelm 2011-08-25 slightly more abstract Command.Perspective;
2011-08-25 wenzelm 2011-08-25 slightly more abstract Text.Perspective;
2011-08-24 wenzelm 2011-08-24 tuned proofs;
2011-08-24 wenzelm 2011-08-24 tuned syntax -- avoid ambiguities;
2011-08-24 wenzelm 2011-08-24 more accurate treatment of index syntax constants, for proper entity references in concrete notation (e.g. infix "\<oplus>\<index>");
2011-08-24 huffman 2011-08-24 delete commented-out dead code
2011-08-24 huffman 2011-08-24 merged
2011-08-24 huffman 2011-08-24 change some subsection headings to subsubsection
2011-08-23 huffman 2011-08-23 remove unnecessary lemma card_ge1
2011-08-23 huffman 2011-08-23 move connected_real_lemma to the one place it is used
2011-08-24 wenzelm 2011-08-24 merged
2011-08-24 blanchet 2011-08-24 make sure that all facts are passed to ATP from minimizer
2011-08-24 blanchet 2011-08-24 more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
2011-08-24 blanchet 2011-08-24 specify timeout for "sledgehammer_tac"
2011-08-24 blanchet 2011-08-24 tuning
2011-08-24 Cezary Kaliszyk 2011-08-24 Quotient Package: add mem_rsp, mem_prs, tune proofs.
2011-08-23 huffman 2011-08-23 merged
2011-08-23 huffman 2011-08-23 declare euclidean_simps [simp] at the point they are proved; avoid duplicate rule warnings;
2011-08-23 huffman 2011-08-23 merged
2011-08-22 huffman 2011-08-22 merged
2011-08-22 huffman 2011-08-22 avoid warnings
2011-08-22 huffman 2011-08-22 comment out dead code to avoid compiler warnings
2011-08-22 huffman 2011-08-22 legacy theorem names
2011-08-22 huffman 2011-08-22 remove duplicate lemma
2011-08-23 blanchet 2011-08-23 fixed "hBOOL" of existential variables, and generate more helpers
2011-08-23 blanchet 2011-08-23 don't select facts when using sledgehammer_tac for reconstruction
2011-08-23 blanchet 2011-08-23 don't perform a triviality check if the goal is skipped anyway
2011-08-23 blanchet 2011-08-23 optional reconstructor
2011-08-24 wenzelm 2011-08-24 misc tuning and simplification;
2011-08-24 wenzelm 2011-08-24 tuned pri: prefer purging of canceled execution;
2011-08-24 wenzelm 2011-08-24 tuned Document.node: maintain "touched" flag to indicate changes in entries etc.;
2011-08-24 wenzelm 2011-08-24 clarified Document.Node.clear -- retain header (cf. ML version);
2011-08-24 wenzelm 2011-08-24 clarified norm_header/header_edit -- disallow update of loaded theories;
2011-08-24 wenzelm 2011-08-24 misc tuning and simplification;