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;
2011-09-04 wenzelm 2011-09-04 moved XML/YXML to src/Pure/PIDE; tuned comments;
2011-09-04 wenzelm 2011-09-04 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 haftmann 2011-09-04 pseudo-definition for perms on sets; tuned
2011-09-03 huffman 2011-09-03 remove duplicate lemma nat_zero in favor of nat_0
2011-09-03 huffman 2011-09-03 merged
2011-09-03 huffman 2011-09-03 merged
2011-09-03 huffman 2011-09-03 modify nominal packages to better respect set/pred distinction
2011-09-03 huffman 2011-09-03 merged
2011-09-03 huffman 2011-09-03 remove unused assumption from lemma posreal_complete
2011-09-03 haftmann 2011-09-03 tuned specifications
2011-09-03 haftmann 2011-09-03 merged
2011-09-03 haftmann 2011-09-03 tuned proof
2011-09-03 haftmann 2011-09-03 merged
2011-09-03 haftmann 2011-09-03 assert Pure equations for theorem references; avoid dynamic reference to fact
2011-09-03 haftmann 2011-09-03 assert Pure equations for theorem references; tuned
2011-09-03 haftmann 2011-09-03 tuned specifications and proofs