2011-09-06 wenzelm 2011-09-06 merged
2011-09-06 huffman 2011-09-06 merged
2011-09-06 huffman 2011-09-06 simplify proof of tan_half, removing unused assumptions
2011-09-06 huffman 2011-09-06 convert some proofs to Isar-style
2011-09-06 blanchet 2011-09-06 added dummy polymorphic THF system
2011-09-06 boehmes 2011-09-06 added some examples for pattern and weight annotations
2011-09-06 bulwahn 2011-09-06 merged
2011-09-06 bulwahn 2011-09-06 avoid "Code" as structure name (cf. 3bc39cfe27fe)
2011-09-06 huffman 2011-09-06 remove duplicate copy of lemma sqrt_add_le_add_sqrt
2011-09-06 huffman 2011-09-06 remove redundant lemma real_sum_squared_expand in favor of power2_sum
2011-09-06 huffman 2011-09-06 remove redundant lemma LIMSEQ_Complex in favor of tendsto_Complex
2011-09-06 huffman 2011-09-06 merged
2011-09-05 huffman 2011-09-05 add lemmas about arctan; simplify some proofs about arctan;
2011-09-05 huffman 2011-09-05 convert lemma cos_total to Isar-style proof
2011-09-06 nipkow 2011-09-06 added new lemmas
2011-09-06 blanchet 2011-09-06 updated Sledgehammer's docs
2011-09-06 blanchet 2011-09-06 cleanup "simple" type encodings
2011-09-06 Cezary Kaliszyk 2011-09-06 merge
2011-09-06 Cezary Kaliszyk 2011-09-06 HOL/Import: Make HOL4 Import work with current Isabelle. Updated constant maps, added bool type map, and tuned compat theorem.
2011-09-06 blanchet 2011-09-06 tuning
2011-09-06 blanchet 2011-09-06 drop more type arguments soundly, when they can be deduced from the arg types
2011-09-06 wenzelm 2011-09-06 bulk reports for improved message throughput;
2011-09-06 wenzelm 2011-09-06 bulk reports for improved message throughput;
2011-09-06 wenzelm 2011-09-06 tuned signature;
2011-09-06 wenzelm 2011-09-06 more specific message channels to avoid potential bottle-neck of raw_messages;
2011-09-06 wenzelm 2011-09-06 buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
2011-09-06 wenzelm 2011-09-06 more abstract receiver interface;
2011-09-06 wenzelm 2011-09-06 flush after Output.raw_message (and init message) for reduced latency of important protocol events;
2011-09-05 huffman 2011-09-05 convert lemma cos_is_zero to Isar-style
2011-09-05 huffman 2011-09-05 merged
2011-09-05 huffman 2011-09-05 convert lemma sin_gt_zero to Isar style; remove duplicate lemma sin_gt_zero1;
2011-09-05 huffman 2011-09-05 modify lemma sums_group, and shorten proofs that use it
2011-09-05 huffman 2011-09-05 generalize some lemmas
2011-09-05 huffman 2011-09-05 add lemmas cos_arctan and sin_arctan
2011-09-05 huffman 2011-09-05 tuned indentation
2011-09-05 wenzelm 2011-09-05 more visible outdated_color;
2011-09-05 wenzelm 2011-09-05 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
2011-09-05 wenzelm 2011-09-05 tuned imports;
2011-09-05 blanchet 2011-09-05 fixed handling of "sledgehammer_params", so that "sledgehammer_params [e]" is really the same as "sledgehammer_params [provers = e]"
2011-09-05 boehmes 2011-09-05 tuned
2011-09-05 boehmes 2011-09-05 tuned
2011-09-05 boehmes 2011-09-05 filter out all schematic theorems if the problem contains no ground constants
2011-09-04 huffman 2011-09-04 merged
2011-09-04 huffman 2011-09-04 tuned comments
2011-09-04 huffman 2011-09-04 simplify proof of Bseq_mono_convergent
2011-09-04 wenzelm 2011-09-04 merged
2011-09-04 huffman 2011-09-04 replace lemma expi_imaginary with reoriented lemma cis_conv_exp
2011-09-04 huffman 2011-09-04 remove redundant lemmas expi_add and expi_zero
2011-09-04 huffman 2011-09-04 remove redundant lemmas about LIMSEQ
2011-09-04 huffman 2011-09-04 introduce abbreviation 'int' earlier in Int.thy
2011-09-04 huffman 2011-09-04 remove unused assumptions from natceiling lemmas
2011-09-04 huffman 2011-09-04 move lemmas nat_le_iff and nat_mono into Int.thy
2011-09-04 wenzelm 2011-09-04 eliminated markup for plain identifiers (frequent but insignificant); reduced "black" markup (outer string etc. takes care of it already);
2011-09-04 wenzelm 2011-09-04 simplified signatures;
2011-09-04 wenzelm 2011-09-04 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
2011-09-04 wenzelm 2011-09-04 tuned document;
2011-09-04 wenzelm 2011-09-04 improved handling of extended styles and hard tabs when prover is inactive;
2011-09-04 wenzelm 2011-09-04 mark hard tabs as single chunks, as required by jEdit;
2011-09-04 wenzelm 2011-09-04 updated READMEs;
2011-09-04 wenzelm 2011-09-04 property "tooltip-dismiss-delay" is edited in ms, not seconds; explicit tooltip_dismiss_delay boundaries for further robustness;