adding type inference for disambiguation annotations in code equation

adding the body type as well to the code generation for constants as it is required for type annotations of constants

changing const type to pass along if typing annotations are necessary for disambigous terms

fixed THF type constructor syntax

tweaking polymorphic TFF and THF output

parse new experimental '@' encodings

tuning

tuning

tuning

clarified import;

tuned/simplified proofs;

tuned proofs;

deactivate unfinished charset provider for now, to avoid user confusion;

more NEWS;

added "check" button: adhoc change to full buffer perspective;

added "cancel" button based on cancel_execution, not interrupt (cf. 156be0e43336);

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

perform mangling before computing symbol arity, to avoid needless "hAPP"s and "hBOOL"s

tuning

make mangling sound w.r.t. type arguments

make "filter_type_args" more robust if the actual arity is higher than the declared one

updated Sledgehammer documentation

rationalize uniform encodings

merged

avoid using legacy theorem names

merged

remove redundant lemmas i_mult_eq and i_mult_eq2 in favor of i_squared

HOL/Import: Update HOL4 generated files to current Isabelle.

tuned proofs;

remove some unnecessary simp rules from simpset

some Isabelle/jEdit NEWS;

more README;

merged

merged

simplify proof of tan_half, removing unused assumptions

convert some proofs to Isar-style

added dummy polymorphic THF system

added some examples for pattern and weight annotations

merged

avoid "Code" as structure name (cf. 3bc39cfe27fe)

remove duplicate copy of lemma sqrt_add_le_add_sqrt

remove redundant lemma real_sum_squared_expand in favor of power2_sum

remove redundant lemma LIMSEQ_Complex in favor of tendsto_Complex

merged

add lemmas about arctan; simplify some proofs about arctan;

convert lemma cos_total to Isar-style proof

added new lemmas

updated Sledgehammer's docs

cleanup "simple" type encodings

merge

HOL/Import: Make HOL4 Import work with current Isabelle. Updated constant maps, added bool type map, and tuned compat theorem.

tuning

drop more type arguments soundly, when they can be deduced from the arg types

bulk reports for improved message throughput;

bulk reports for improved message throughput;

tuned signature;

more specific message channels to avoid potential bottle-neck of raw_messages;

buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;

more abstract receiver interface;

flush after Output.raw_message (and init message) for reduced latency of important protocol events;

convert lemma cos_is_zero to Isar-style

merged

convert lemma sin_gt_zero to Isar style; remove duplicate lemma sin_gt_zero1;

modify lemma sums_group, and shorten proofs that use it

generalize some lemmas

add lemmas cos_arctan and sin_arctan

tuned indentation

more visible outdated_color;

commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;

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