isabelle: Graph

Mercurial Mercurial > repos > isabelle / graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip

HOL/Import: Update HOL4 generated files to current Isabelle.
2011-09-07, by Cezary Kaliszyk
tuned proofs;
2011-09-07, by wenzelm
remove some unnecessary simp rules from simpset
2011-09-06, by huffman
some Isabelle/jEdit NEWS;
2011-09-06, by wenzelm
more README;
2011-09-06, by wenzelm
merged
2011-09-06, by wenzelm
merged
2011-09-06, by huffman
simplify proof of tan_half, removing unused assumptions
2011-09-06, by huffman
convert some proofs to Isar-style
2011-09-06, by huffman
added dummy polymorphic THF system
2011-09-06, by blanchet
added some examples for pattern and weight annotations
2011-09-06, by boehmes
merged
2011-09-06, by bulwahn
avoid "Code" as structure name (cf. 3bc39cfe27fe)
2011-09-06, by bulwahn
remove duplicate copy of lemma sqrt_add_le_add_sqrt
2011-09-06, by huffman
remove redundant lemma real_sum_squared_expand in favor of power2_sum
2011-09-06, by huffman
remove redundant lemma LIMSEQ_Complex in favor of tendsto_Complex
2011-09-06, by huffman
merged
2011-09-06, by huffman
add lemmas about arctan;
2011-09-05, by huffman
convert lemma cos_total to Isar-style proof
2011-09-05, by huffman
added new lemmas
2011-09-06, by nipkow
updated Sledgehammer's docs
2011-09-06, by blanchet
cleanup "simple" type encodings
2011-09-06, by blanchet
merge
2011-09-06, by Cezary Kaliszyk
HOL/Import: Make HOL4 Import work with current Isabelle. Updated constant maps, added bool type map, and tuned compat theorem.
2011-09-06, by Cezary Kaliszyk
tuning
2011-09-06, by blanchet
drop more type arguments soundly, when they can be deduced from the arg types
2011-09-06, by blanchet
bulk reports for improved message throughput;
2011-09-06, by wenzelm
bulk reports for improved message throughput;
2011-09-06, by wenzelm
tuned signature;
2011-09-06, by wenzelm
more specific message channels to avoid potential bottle-neck of raw_messages;
2011-09-06, by wenzelm
buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
2011-09-06, by wenzelm
more abstract receiver interface;
2011-09-06, by wenzelm
flush after Output.raw_message (and init message) for reduced latency of important protocol events;
2011-09-06, by wenzelm
convert lemma cos_is_zero to Isar-style
2011-09-05, by huffman
merged
2011-09-05, by huffman
convert lemma sin_gt_zero to Isar style;
2011-09-05, by huffman
modify lemma sums_group, and shorten proofs that use it
2011-09-05, by huffman
generalize some lemmas
2011-09-05, by huffman
add lemmas cos_arctan and sin_arctan
2011-09-05, by huffman
tuned indentation
2011-09-05, by huffman
more visible outdated_color;
2011-09-05, by wenzelm
commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
2011-09-05, by wenzelm
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

less more | (0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip

isabelle