2011-09-07 blanchet 2011-09-07 make mangling sound w.r.t. type arguments
2011-09-07 blanchet 2011-09-07 make "filter_type_args" more robust if the actual arity is higher than the declared one
2011-09-07 blanchet 2011-09-07 updated Sledgehammer documentation
2011-09-07 blanchet 2011-09-07 rationalize uniform encodings
2011-09-06 huffman 2011-09-06 merged
2011-09-06 huffman 2011-09-06 avoid using legacy theorem names
2011-09-06 huffman 2011-09-06 merged
2011-09-06 huffman 2011-09-06 remove redundant lemmas i_mult_eq and i_mult_eq2 in favor of i_squared
2011-09-07 Cezary Kaliszyk 2011-09-07 HOL/Import: Update HOL4 generated files to current Isabelle.
2011-09-07 wenzelm 2011-09-07 tuned proofs;
2011-09-06 huffman 2011-09-06 remove some unnecessary simp rules from simpset
2011-09-06 wenzelm 2011-09-06 some Isabelle/jEdit NEWS;
2011-09-06 wenzelm 2011-09-06 more README;
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