isabelle: Graph

improve completeness of polymorphic encodings
2011-08-26, by blanchet
mangle tag bound declarations properly
2011-08-26, by blanchet
fixed inverted logic and improve precision when handling monotonic types in polymorphic encodings
2011-08-26, by blanchet
make sure that if slicing is disabled, a non-SOS slice is chosen
2011-08-25, by blanchet
honor TFF Implicit
2011-08-25, by blanchet
make polymorphic encodings more complete
2011-08-25, by blanchet
make default unsound mode less unsound
2011-08-25, by blanchet
make TFF output less explicit where possible
2011-08-25, by blanchet
use more appropriate encoding for Z3 TPTP, as confirmed by evaluation
2011-08-25, by blanchet
added one more known Z3 failure
2011-08-25, by blanchet
added config options to control two aspects of the translation, for evaluation purposes
2011-08-25, by blanchet
added choice operator output for
2011-08-25, by nik
rationalized option names -- mono becomes raw_mono and mangled becomes mono
2011-08-25, by blanchet
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, by blanchet
avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
2011-08-25, by blanchet
fixed bang encoding detection of which types to encode
2011-08-25, by blanchet
lemma Compl_insert: "- insert x A = (-A) - {x}"
2011-08-25, by krauss
avoid variable clashes by properly incrementing indices
2011-08-25, by boehmes
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
2011-08-25, by boehmes
include chained facts for minimizer, otherwise it won't work
2011-08-25, by blanchet
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-24, by blanchet
back to tradition Scratch.thy default -- execution wrt. perspective overcomes the main problems of 226563829580;
2011-08-26, by wenzelm
tuned Session.edit_node: update_perspective based on last_exec_offset;
2011-08-26, by wenzelm
tuned signature -- iterate subsumes both fold and get_first;
2011-08-26, by wenzelm
further clarification of Document.updated, based on last_common and after_entry;
2011-08-26, by wenzelm
tuned signature;
2011-08-26, by wenzelm
improved Document.edit: more accurate update_start and no_execs;
2011-08-26, by wenzelm
refined document state assignment: observe perspective, more explicit assignment message;
2011-08-26, by wenzelm
tuned signature -- emphasize traditional read/eval/print terminology, which is still relevant here;
2011-08-25, by wenzelm
maintain last_execs assignment on Scala side;
2011-08-25, by wenzelm
propagate information about last command with exec state assignment through document model;
2011-08-25, by wenzelm
tuned signature;
2011-08-25, by wenzelm
slightly more abstract Command.Perspective;
2011-08-25, by wenzelm
slightly more abstract Text.Perspective;
2011-08-25, by wenzelm
tuned proofs;
2011-08-24, by wenzelm
tuned syntax -- avoid ambiguities;
2011-08-24, by wenzelm
more accurate treatment of index syntax constants, for proper entity references in concrete notation (e.g. infix "\<oplus>\<index>");
2011-08-24, by wenzelm
delete commented-out dead code
2011-08-24, by huffman
merged
2011-08-24, by huffman
change some subsection headings to subsubsection
2011-08-24, by huffman
remove unnecessary lemma card_ge1
2011-08-23, by huffman
move connected_real_lemma to the one place it is used
2011-08-23, by huffman
merged
2011-08-24, by wenzelm
make sure that all facts are passed to ATP from minimizer
2011-08-24, by blanchet
more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
2011-08-24, by blanchet
specify timeout for "sledgehammer_tac"
2011-08-24, by blanchet
tuning
2011-08-24, by blanchet
Quotient Package: add mem_rsp, mem_prs, tune proofs.
2011-08-24, by Cezary Kaliszyk
merged
2011-08-23, by huffman
declare euclidean_simps [simp] at the point they are proved;
2011-08-23, by huffman
merged
2011-08-23, by huffman
merged
2011-08-22, by huffman
avoid warnings
2011-08-22, by huffman
comment out dead code to avoid compiler warnings
2011-08-22, by huffman
legacy theorem names
2011-08-22, by huffman
remove duplicate lemma
2011-08-22, by huffman
fixed "hBOOL" of existential variables, and generate more helpers
2011-08-23, by blanchet
don't select facts when using sledgehammer_tac for reconstruction
2011-08-23, by blanchet
don't perform a triviality check if the goal is skipped anyway
2011-08-23, by blanchet
optional reconstructor
2011-08-23, by blanchet
misc tuning and simplification;
2011-08-24, by wenzelm
tuned pri: prefer purging of canceled execution;
2011-08-24, by wenzelm
tuned Document.node: maintain "touched" flag to indicate changes in entries etc.;
2011-08-24, by wenzelm
clarified Document.Node.clear -- retain header (cf. ML version);
2011-08-24, by wenzelm
clarified norm_header/header_edit -- disallow update of loaded theories;
2011-08-24, by wenzelm
misc tuning and simplification;
2011-08-24, by wenzelm
ignore irrelevant timings;
2011-08-24, by wenzelm
print state only for visible command, to avoid wasting resources for the larger part of the text;
2011-08-24, by wenzelm
early filtering of unchanged perspective;
2011-08-24, by wenzelm
more reliable update_perspective handler based on actual text visibility (e.g. on startup or when resizing without scrolling);
2011-08-24, by wenzelm
update_perspective without actual edits, bypassing the full state assignment protocol;
2011-08-24, by wenzelm
tuned;
2011-08-23, by wenzelm
handle potentially more approriate BufferUpdate.LOADED event;
2011-08-23, by wenzelm
special treatment of structure index 1 in Pure, including legacy warning;
2011-08-22, by wenzelm
compile
2011-08-23, by blanchet
added "max_calls" option to get a fixed number of Sledgehammer calls per theory
2011-08-23, by blanchet
beef up "sledgehammer_tac" reconstructor
2011-08-23, by blanchet
clean up Sledgehammer tactic
2011-08-23, by blanchet
fixed document;
2011-08-23, by wenzelm
tuned signature;
2011-08-23, by wenzelm
merged
2011-08-23, by wenzelm
always use TFF if possible
2011-08-23, by blanchet
clearer separator in generated file names
2011-08-23, by blanchet
exploit TFF format in Z3 used as ATP, and renamed it "z3_tptp"
2011-08-23, by blanchet
updated known failures for Z3 3.0 TPTP
2011-08-23, by blanchet
updated Z3 docs
2011-08-23, by blanchet
avoid TFF format with older Vampire versions
2011-08-23, by blanchet
update the Vampire related parts of the documentation
2011-08-23, by blanchet
fixed TFF slicing
2011-08-23, by blanchet
kindly ask Vampire to output axiom names
2011-08-23, by blanchet
added formats to the slice and use TFF for remote Vampire
2011-08-23, by blanchet
tuned specifications, syntax and proofs
2011-08-23, by haftmann
tuned specifications and syntax
2011-08-22, by haftmann
Quotient Package: some infrastructure for lifting inside sets
2011-08-23, by Cezary Kaliszyk
include all encodings in tests, now that the incompleteness of some encodings has been addressed
2011-08-22, by blanchet
change Metis's default settings if type information axioms are generated
2011-08-22, by blanchet
we must tag any type whose ground types intersect a nonmonotonic type
2011-08-22, by blanchet
prefer the lighter, slightly unsound monotonicity-based encodings for Metis
2011-08-22, by blanchet
made reconstruction of type tag equalities "\?x = \?x" reliable
2011-08-22, by blanchet
tuning ATP problem output
2011-08-22, by blanchet
revert guard logic -- make sure that typing information is generated for existentials
2011-08-22, by blanchet
generate tag equations for existential variables
2011-08-22, by blanchet
tuning, plus started implementing tag equation generation for existential variables
2011-08-22, by blanchet
precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis
2011-08-22, by blanchet
clearer terminology
2011-08-22, by blanchet
renamed "heavy" to "uniform", based on discussion with Nick Smallbone
2011-08-22, by blanchet
removed unused configuration option
2011-08-22, by blanchet
added caching for (in)finiteness checks
2011-08-22, by blanchet
remove needless typing information
2011-08-22, by blanchet
cleaner handling of polymorphic monotonicity inference
2011-08-22, by blanchet
started cleaning up polymorphic monotonicity-based encodings, based on discussions with Nick Smallbone
2011-08-22, by blanchet
more precise warning
2011-08-22, by blanchet
added option to control soundness of encodings more precisely, for evaluation purposes
2011-08-22, by blanchet
make sound mode more sound (and clean up code)
2011-08-22, by blanchet
reintroduced slightly unsound optimization taken out in 717880e98e6b, but only if "sound" is false
2011-08-22, by blanchet
gracefully handle empty SPASS problems
2011-08-22, by blanchet
pass sound option to Sledgehammer tactic
2011-08-22, by blanchet
tuned signature -- contrast physical output primitives versus Output.raw_message;
2011-08-23, by wenzelm
tuned signature;
2011-08-23, by wenzelm
discontinued slightly odd Future/Lazy.get_finished, which do not really fit into the execution model of Future.cancel/join_tasks (canceled tasks need to be dequeued and terminated explicitly);
2011-08-23, by wenzelm