tuned imports;

fixed handling of "sledgehammer_params", so that "sledgehammer_params [e]" is really the same as "sledgehammer_params [provers = e]"

tuned

tuned

filter out all schematic theorems if the problem contains no ground constants

merged

tuned comments

simplify proof of Bseq_mono_convergent

merged

replace lemma expi_imaginary with reoriented lemma cis_conv_exp

remove redundant lemmas expi_add and expi_zero

remove redundant lemmas about LIMSEQ

introduce abbreviation 'int' earlier in Int.thy

remove unused assumptions from natceiling lemmas

move lemmas nat_le_iff and nat_mono into Int.thy

eliminated markup for plain identifiers (frequent but insignificant); reduced "black" markup (outer string etc. takes care of it already);

simplified signatures;

synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;

tuned document;

improved handling of extended styles and hard tabs when prover is inactive;

mark hard tabs as single chunks, as required by jEdit;

updated READMEs;

property "tooltip-dismiss-delay" is edited in ms, not seconds; explicit tooltip_dismiss_delay boundaries for further robustness;

moved XML/YXML to src/Pure/PIDE; tuned comments;

pass raw messages through xml_cache actor, which is important to retain ordering of results (e.g. read_command reports before assign, cf. 383c9d758a56);

pseudo-definition for perms on sets; tuned

remove duplicate lemma nat_zero in favor of nat_0

merged

merged

modify nominal packages to better respect set/pred distinction

merged

remove unused assumption from lemma posreal_complete

tuned specifications

merged

tuned proof

merged

assert Pure equations for theorem references; avoid dynamic reference to fact

assert Pure equations for theorem references; tuned

tuned specifications and proofs

merged

remove duplicate lemma finite_choice in favor of finite_set_choice

simplify proof

shorten some proofs

remove redundant simp rules ceiling_floor and floor_ceiling

misc tuning and simplification of proofs;

Document.removed_versions on Scala side;

discontinued predefined empty command (obsolete!?);

discontinued global execs: store exec value directly within entries; simplified entries: no extra copy of command_id;

Document.remove_versions on ML side;

some support to prune_history; clarified signature: recent_stable is supposed to be always defined;

merged

speed up extremely slow metis proof of Sup_real_iff (reducing total HOL compilation time by 5% on my machine)

remove redundant lemma reals_complete2 in favor of complete_real

simplify proof of Rats_dense_in_real; remove lemma Rats_dense_in_nn_real;

remove unused, unnecessary lemmas

remove more duplicate lemmas

merged

merged

avoid "Code" as structure name

more robust chunk painting wrt. hard tabs, when chunk.str == null;

raw message function "assign_execs" avoids full overhead of decoding and caching message body;

less agressive parsing of commands (priority ~1); join commands just before actual assignment;

tuned;

more direct Token.range_pos and Outer_Syntax.read_command, bypassing Thy_Syntax.span;

merged

Added Abstract Interpretation theories

tuned proofs;

proper config option linarith_trace;

discontinued slightly odd "Defining record ..." message and corresponding quiet_mode;

merged

renamed "Metis_Tactics" to "Metis_Tactic", now that there is only one Metis tactic ("metisFT" is legacy)

use new syntax for Pi binder in TFF1 output

fewer TPTP important messages

simplify some proofs about uniform continuity, and add some new ones; rename some theorems according to standard naming scheme;

modernize lemmas about 'continuous' and 'continuous_on'; improve automation of continuity proofs;

add lemma tendsto_infnorm

more precise iterate_entries_after if start refers to last entry; do not assign exec states after bad theory init; reject illegal theory header after end of theory;

clarified define_command: store name as structural information;

amended last_common, if that happens to the very last entry (important to load HOL/Auth, for example); clarified touch_node: reset result explicitly;

more redable Document.Node.toString;

sort wrt. theory name;

modernized theory name;

repaired benchmarks;

merged

tuning

always measure time for ATPs -- auto minimization relies on it

added two lemmas about "distinct" to help Sledgehammer

make "sound" sound and "unsound" more sound, based on evaluation

HOL/Import: observe distinction between sets and predicates (where possible)

simplify/generalize some proofs

generalize lemma isCont_vec_nth

convert proof to Isar-style

remove redundant lemma card_enum

move lemmas from Topology_Euclidean_Space to Euclidean_Space

convert to Isar-style proof

make SML/NJ happy

more tuning

more tuning

tuning

avoid relying on dubious TFF1 feature

killed FIXME (the ATP exporter outputs TPTP FOF, which is first-order)

fixed explicit declaration of TFF1 types

adding list_size_append (thanks to Rene Thiemann)

strengthening list_size_pointwise (thanks to Rene Thiemann)

more flexible sorting; tuned display;

tuned signature;

more abstract Document.Node.Name; tuned signature;

more careful treatment of interrupts, to retain them within forked/joined boundary of command transactions;

crude display of node status; tuned signature;

explicit cancel_execution before queueing new edits -- potential performance improvement for machines with few cores;

explicit running_color; stronger colors for overview, more transparent colors for status within text;

tuned join_commands: avoid traversing cumulative table;

some support for theory status overview;

tuned Commands_Changed: cover nodes as well;

maintain name of *the* enclosing node as part of command -- avoid full document traversal;

improved auto loading: selectable file list;

tuned document;

tuned import; discontinued obsolete Sorting.thy (cf. 4d57f872dc2c);

tuned document;

tuned color for Mac OS X (very light color profile?);