2011-09-07 blanchet 2011-09-07 tuning
2011-09-07 blanchet 2011-09-07 tuning
2011-09-07 wenzelm 2011-09-07 clarified import;
2011-09-07 wenzelm 2011-09-07 tuned/simplified proofs;
2011-09-07 wenzelm 2011-09-07 tuned proofs;
2011-09-07 wenzelm 2011-09-07 deactivate unfinished charset provider for now, to avoid user confusion;
2011-09-07 wenzelm 2011-09-07 more NEWS;
2011-09-07 wenzelm 2011-09-07 added "check" button: adhoc change to full buffer perspective;
2011-09-07 wenzelm 2011-09-07 added "cancel" button based on cancel_execution, not interrupt (cf. 156be0e43336);
2011-09-07 blanchet 2011-09-07 separate mangling, which can (and should) be done before the formulas are first-orderized, and type arg filtering, which must be done after once the min arities have been computed
2011-09-07 blanchet 2011-09-07 perform mangling before computing symbol arity, to avoid needless "hAPP"s and "hBOOL"s
2011-09-07 blanchet 2011-09-07 tuning
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