isabelle: Graph

tuned
2011-08-28, by haftmann
split timeout among ATPs in and add Metis to the mix as backup
2011-08-28, by blanchet
more portable cp options, e.g. for non-GNU version on Mac OS X Leopard;
2011-08-28, by wenzelm
tuned positions of ambiguity messages -- less intrusive in IDE view;
2011-08-28, by wenzelm
tuned
2011-08-28, by haftmann
merged
2011-08-28, by haftmann
avoid loading List_Cset and Dlist_Cet at the same time
2011-08-28, by haftmann
corrected slip
2011-08-28, by haftmann
Cset, Dlist_Cset, List_Cset: restructured
2011-08-27, by haftmann
Cset, Dlist_Cset, List_Cset: restructured
2011-08-27, by haftmann
adapted to changes in Cset.thy
2011-08-27, by haftmann
adapted to changes in Cset.thy
2011-08-26, by haftmann
separating predicates and sets syntactically
2011-08-26, by haftmann
merged
2011-08-26, by haftmann
avoid intermixing set and predicates; dropped lemmas mem_rsp and mem_prs (now in Quotient_Set.thy)
2011-08-26, by haftmann
updated generated files
2011-08-25, by haftmann
merged
2011-08-25, by haftmann
updated generated files
2011-08-25, by haftmann
explicit markup for legacy warnings;
2011-08-27, by wenzelm
updated generated files;
2011-08-27, by wenzelm
less aggressive warning icon;
2011-08-27, by wenzelm
tuned colors;
2011-08-27, by wenzelm
transparent foreground color for quoted entities;
2011-08-27, by wenzelm
more precise treatment of nodes that are fully required for partially visible ones;
2011-08-27, by wenzelm
de-assigned commands also count as changed;
2011-08-27, by wenzelm
beef up sledgehammer_tac in Mirabelle some more
2011-08-27, by blanchet
merged
2011-08-27, by blanchet
change default for generation of tag idempotence and tag argument equations
2011-08-26, by blanchet
merged
2011-08-26, by huffman
NEWS entry for setsum_norm ~> norm_setsum
2011-08-26, by huffman
make HOL-Probability respect set/pred distinction
2011-08-26, by huffman
merged
2011-08-26, by wenzelm
use rename_tac to make proof script more robust (with separate set type, 'clarify' yields different variable names)
2010-09-08, by huffman
merged
2011-08-26, by huffman
generalize and simplify proof of continuous_within_sequentially
2011-08-26, by huffman
add lemma sequentially_imp_eventually_within;
2011-08-26, by huffman
replace some continuous_on lemmas with more general versions
2011-08-25, by huffman
remove legacy theorem Lim_inner
2011-08-25, by huffman
arrange everything related to ordered_euclidean_space class together
2011-08-25, by huffman
generalize and shorten proof of basis_orthogonal
2011-08-25, by huffman
remove dot_lsum and dot_rsum in favor of inner_setsum_{left,right}
2011-08-25, by huffman
merged
2011-08-25, by huffman
generalize lemma finite_imp_compact_convex_hull and related lemmas
2011-08-25, by huffman
generalize some lemmas
2011-08-25, by huffman
generalize lemma convex_cone_hull
2011-08-25, by huffman
rename subset_{interior,closure} to {interior,closure}_mono;
2011-08-25, by huffman
simplify many proofs about subspace and span;
2011-08-25, by huffman
remove duplicate simp declaration
2011-08-25, by huffman
simplify definition of 'interior';
2011-08-25, by huffman
add lemma closure_union;
2011-08-24, by huffman
minimize imports
2011-08-24, by huffman
move everything related to 'norm' method into new theory file Norm_Arith.thy
2011-08-24, by huffman
remove unused lemmas dimensionI, dimension_eq
2011-08-24, by huffman
move geometric progression lemmas from Linear_Algebra.thy to Integration.thy where they are used
2011-08-24, by huffman
merge
2011-08-26, by Cezary Kaliszyk
FSet: Explicit proof without mem_def
2011-08-26, by Cezary Kaliszyk
merged
2011-08-26, by nipkow
added lemma
2011-08-26, by nipkow
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
2011-08-26, by blanchet
comment
2011-08-26, by blanchet
disable TFF for Vampire 1.8 until they've fixed the soundness issues and it's back on SystemOnTPTP
2011-08-26, by blanchet
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