isabelle: Graph

tuned imports;
2011-09-05, by wenzelm
fixed handling of "sledgehammer_params", so that "sledgehammer_params [e]" is really the same as "sledgehammer_params [provers = e]"
2011-09-05, by blanchet
tuned
2011-09-05, by boehmes
tuned
2011-09-05, by boehmes
filter out all schematic theorems if the problem contains no ground constants
2011-09-05, by boehmes
merged
2011-09-04, by huffman
tuned comments
2011-09-04, by huffman
simplify proof of Bseq_mono_convergent
2011-09-04, by huffman
merged
2011-09-04, by wenzelm
replace lemma expi_imaginary with reoriented lemma cis_conv_exp
2011-09-04, by huffman
remove redundant lemmas expi_add and expi_zero
2011-09-04, by huffman
remove redundant lemmas about LIMSEQ
2011-09-04, by huffman
introduce abbreviation 'int' earlier in Int.thy
2011-09-04, by huffman
remove unused assumptions from natceiling lemmas
2011-09-04, by huffman
move lemmas nat_le_iff and nat_mono into Int.thy
2011-09-04, by huffman
eliminated markup for plain identifiers (frequent but insignificant);
2011-09-04, by wenzelm
simplified signatures;
2011-09-04, by wenzelm
synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
2011-09-04, by wenzelm
tuned document;
2011-09-04, by wenzelm
improved handling of extended styles and hard tabs when prover is inactive;
2011-09-04, by wenzelm
mark hard tabs as single chunks, as required by jEdit;
2011-09-04, by wenzelm
updated READMEs;
2011-09-04, by wenzelm
property "tooltip-dismiss-delay" is edited in ms, not seconds;
2011-09-04, by wenzelm
moved XML/YXML to src/Pure/PIDE;
2011-09-04, by wenzelm
pass raw messages through xml_cache actor, which is important to retain ordering of results (e.g. read_command reports before assign, cf. 383c9d758a56);
2011-09-04, by wenzelm
pseudo-definition for perms on sets; tuned
2011-09-04, by haftmann
remove duplicate lemma nat_zero in favor of nat_0
2011-09-03, by huffman
merged
2011-09-03, by huffman
merged
2011-09-03, by huffman
modify nominal packages to better respect set/pred distinction
2011-09-03, by huffman
merged
2011-09-03, by huffman
remove unused assumption from lemma posreal_complete
2011-09-03, by huffman
tuned specifications
2011-09-03, by haftmann
merged
2011-09-03, by haftmann
tuned proof
2011-09-03, by haftmann
merged
2011-09-03, by haftmann
assert Pure equations for theorem references; avoid dynamic reference to fact
2011-09-03, by haftmann
assert Pure equations for theorem references; tuned
2011-09-03, by haftmann
tuned specifications and proofs
2011-09-03, by haftmann
merged
2011-09-03, by wenzelm
remove duplicate lemma finite_choice in favor of finite_set_choice
2011-09-03, by huffman
simplify proof
2011-09-03, by huffman
shorten some proofs
2011-09-03, by huffman
remove redundant simp rules ceiling_floor and floor_ceiling
2011-09-02, by huffman
misc tuning and simplification of proofs;
2011-09-03, by wenzelm
Document.removed_versions on Scala side;
2011-09-03, by wenzelm
discontinued predefined empty command (obsolete!?);
2011-09-03, by wenzelm
discontinued global execs: store exec value directly within entries;
2011-09-03, by wenzelm
Document.remove_versions on ML side;
2011-09-03, by wenzelm
some support to prune_history;
2011-09-03, by wenzelm
merged
2011-09-02, by huffman
speed up extremely slow metis proof of Sup_real_iff
2011-09-02, by huffman
remove redundant lemma reals_complete2 in favor of complete_real
2011-09-02, by huffman
simplify proof of Rats_dense_in_real;
2011-09-02, by huffman
remove unused, unnecessary lemmas
2011-09-02, by huffman
remove more duplicate lemmas
2011-09-02, by huffman
merged
2011-09-02, by wenzelm
merged
2011-09-02, by haftmann
avoid "Code" as structure name
2011-09-02, by haftmann
more robust chunk painting wrt. hard tabs, when chunk.str == null;
2011-09-02, by wenzelm
raw message function "assign_execs" avoids full overhead of decoding and caching message body;
2011-09-02, by wenzelm
less agressive parsing of commands (priority ~1);
2011-09-02, by wenzelm
tuned;
2011-09-02, by wenzelm
more direct Token.range_pos and Outer_Syntax.read_command, bypassing Thy_Syntax.span;
2011-09-02, by wenzelm
merged
2011-09-02, by nipkow
Added Abstract Interpretation theories
2011-09-02, by nipkow
tuned proofs;
2011-09-02, by wenzelm
proper config option linarith_trace;
2011-09-02, by wenzelm
discontinued slightly odd "Defining record ..." message and corresponding quiet_mode;
2011-09-02, by wenzelm
merged
2011-09-02, by wenzelm
renamed "Metis_Tactics" to "Metis_Tactic", now that there is only one Metis tactic ("metisFT" is legacy)
2011-09-02, by blanchet
use new syntax for Pi binder in TFF1 output
2011-09-02, by blanchet
fewer TPTP important messages
2011-09-02, by blanchet
simplify some proofs about uniform continuity, and add some new ones;
2011-09-01, by huffman
modernize lemmas about 'continuous' and 'continuous_on';
2011-09-01, by huffman
add lemma tendsto_infnorm
2011-09-01, by huffman
more precise iterate_entries_after if start refers to last entry;
2011-09-02, by wenzelm
clarified define_command: store name as structural information;
2011-09-02, by wenzelm
amended last_common, if that happens to the very last entry (important to load HOL/Auth, for example);
2011-09-01, by wenzelm
more redable Document.Node.toString;
2011-09-01, by wenzelm
sort wrt. theory name;
2011-09-01, by wenzelm
modernized theory name;
2011-09-01, by wenzelm
repaired benchmarks;
2011-09-01, by wenzelm
merged
2011-09-01, by wenzelm
tuning
2011-09-01, by blanchet
always measure time for ATPs -- auto minimization relies on it
2011-09-01, by blanchet
added two lemmas about "distinct" to help Sledgehammer
2011-09-01, by blanchet
make "sound" sound and "unsound" more sound, based on evaluation
2011-09-01, by blanchet
HOL/Import: observe distinction between sets and predicates (where possible)
2011-09-01, by Cezary Kaliszyk
simplify/generalize some proofs
2011-08-31, by huffman
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
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