isabelle: Graph

generalize lemma isCont_vec_nth
2011-08-31, by huffman
convert proof to Isar-style
2011-08-31, by huffman
remove redundant lemma card_enum
2011-08-31, by huffman
move lemmas from Topology_Euclidean_Space to Euclidean_Space
2011-08-31, by huffman
convert to Isar-style proof
2011-08-31, by huffman
make SML/NJ happy
2011-08-31, by blanchet
more tuning
2011-08-31, by blanchet
more tuning
2011-08-31, by blanchet
tuning
2011-08-31, by blanchet
avoid relying on dubious TFF1 feature
2011-08-31, by blanchet
killed FIXME (the ATP exporter outputs TPTP FOF, which is first-order)
2011-08-31, by blanchet
fixed explicit declaration of TFF1 types
2011-08-31, by blanchet
adding list_size_append (thanks to Rene Thiemann)
2011-08-30, by bulwahn
strengthening list_size_pointwise (thanks to Rene Thiemann)
2011-08-30, by bulwahn
more flexible sorting;
2011-09-01, by wenzelm
tuned signature;
2011-09-01, by wenzelm
more abstract Document.Node.Name;
2011-09-01, by wenzelm
more careful treatment of interrupts, to retain them within forked/joined boundary of command transactions;
2011-09-01, by wenzelm
crude display of node status;
2011-08-31, by wenzelm
explicit cancel_execution before queueing new edits -- potential performance improvement for machines with few cores;
2011-08-31, by wenzelm
explicit running_color;
2011-08-31, by wenzelm
tuned join_commands: avoid traversing cumulative table;
2011-08-31, by wenzelm
some support for theory status overview;
2011-08-31, by wenzelm
tuned Commands_Changed: cover nodes as well;
2011-08-31, by wenzelm
maintain name of *the* enclosing node as part of command -- avoid full document traversal;
2011-08-31, by wenzelm
improved auto loading: selectable file list;
2011-08-31, by wenzelm
tuned document;
2011-08-30, by wenzelm
tuned import;
2011-08-30, by wenzelm
tuned document;
2011-08-30, by wenzelm
tuned color for Mac OS X (very light color profile?);
2011-08-30, by wenzelm
tuned document;
2011-08-30, by wenzelm
merged;
2011-08-30, by wenzelm
fixed just introduced silly bug
2011-08-30, by blanchet
"simple" was renamed "mono_simple" and there's now "poly_simple" as well -- but they are not needed here since for Metis they amount to the same as guards
2011-08-30, by blanchet
tuning
2011-08-30, by blanchet
cleaner "pff" dummy TFF0 prover
2011-08-30, by blanchet
generate properly typed TFF1 (PFF) problems in the presence of type class predicates
2011-08-30, by blanchet
added type abstractions (for declaring polymorphic constants) to TFF syntax
2011-08-30, by blanchet
implement more of the polymorphic simply typed format TFF(1)
2011-08-30, by blanchet
flip logic of boolean option so it's off by default
2011-08-30, by blanchet
extended simple types with polymorphism -- the implementation still needs some work though
2011-08-30, by blanchet
added dummy PFF prover, for debugging purposes
2011-08-30, by blanchet
first step towards polymorphic TFF + changed defaults for Vampire
2011-08-30, by blanchet
tuning
2011-08-30, by blanchet
removed explicit reliance on Hilbert_Choice.Eps
2011-08-30, by nik
improved handling of induction rules in Sledgehammer
2011-08-30, by nik
added generation of induction rules
2011-08-30, by nik
simplify some proofs
2011-08-29, by huffman
restrict perspective to actual buffer_range, to avoid spurious edits due to faulty last_exec_offset (NB: jEdit screenlines may be silently extended by trailing newline);
2011-08-30, by wenzelm
tuned signature;
2011-08-30, by wenzelm
dynamic exec state lookup for implicit position information (e.g. 'definition' without binding);
2011-08-30, by wenzelm
some support for hyperlinks between different buffers;
2011-08-30, by wenzelm
tuned colors -- more distance between outdated_color and quoted_color;
2011-08-30, by wenzelm
do not normalized extra file dependencies for now -- still loaded by prover process;
2011-08-30, by wenzelm
separate module for jEdit primitives for loading theory files;
2011-08-30, by wenzelm
merged
2011-08-29, by wenzelm
Product_Vector.thy: clean up some proofs
2011-08-29, by huffman
actual auto loading of required files;
2011-08-29, by wenzelm
some dialog for auto loading of required files (still inactive);
2011-08-29, by wenzelm
invoke in Swing thread to make double sure;
2011-08-29, by wenzelm
move class perfect_space into RealVector.thy;
2011-08-28, by huffman
generalize LIM_zero lemmas to arbitrary filters
2011-08-28, by huffman
merged
2011-08-28, by huffman
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
2011-08-28, by huffman
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