protocol support for thread debugger state;

eliminated clone;

merged

more symbols; more spaces;

more symbols;

more documentation of coercions

merged

clarified management of (single) session; proper Debugger.Update events;

maintain debugger output messages;

provide CharSequence operations as well;

more GUI components;

tuned;

separate channel for debugger output; clarified thread name;

clarified thread name;

add coinduction rule for infinite

merged

clarified context;

more explicit context; tuned signature;

eliminated dead code;

clarified Variable.gen_all; simplified Local_Defs.export: pointless partial application;

more explicit context;

more direct access to atomic cterms;

clarified context;

proper context;

more direct access to atomic cterms;

clarified context;

clarified context;

clarified context;

merged

merged

added theory Uniform_Limit

evade timeout problem on macbroy6 (potentially due to NFS oddities);

tweaks. Got rid of a really slow step

the Cauchy integral theorem and related material

depth -> height; removed del_rightmost (too specifi)

tuned;

merged

tuned signature; clarified context;

formal class for factorial (semi)rings

merged

NEWS;

tuned signature;

New material for Cauchy's integral theorem

tuned signature for print_nested_cases;

more explicit checks -- improved errors;

eliminated cterm_instantiate;

updated to infer_instantiate; clarified context;

tuned signature;

added infer_instantiate_vars, which allows inconsistent types for variables, as required for Metis proof reconstruction;

eliminated atac, rtac, etac, dtac, ftac;

updated to infer_instantiate;

updated to infer_instantiate;

updated to infer_instantiate;

proper context;

updated to infer_instantiate;

updated to infer_instantiate; clarified context;

ignore non-existant variables, like other instantiate rules;

updated to infer_instantiate;

updated to infer_instantiate;

added infer_instantiate'; clarified boundary cases of instantiate';

more uniform exceptions, like cterm_instantiate;

updated to infer_instantiate; tuned;

more accurate maxidx;

clarified error;

added infer_instantiate, which is meant to supersede cterm_instantiate;

eliminated alias;

proper context;

unused;

proper context;

more symbols by default, without xsymbols mode;

Measures form a CCPO

reorganized Extended_Real

isabelle update_cartouches;

tuned proofs;

proper latex;

tuned proofs;

tuned proofs;

support for ML debugger;

more explicit thread identification;

avoid lxbroy2, lxbroy3, lxbroy4, which are often busy with other processes;

new material for multivariate analysis, etc.

proper LaTeX;

updated to jdk-8u51;

more symbols;

isabelle update_cartouches;

prefer tactics with explicit context;

prefer tactics with explicit context;

merged

prefer tactics with explicit context;

tuned whitespace;

prefer tactics with explicit context;

reactivated dead code;

more uniform ComponentAdapter;

skeleton for interactive debugger;

tuned;

tuned;

store breakpoints within ML environment;

clarified ML compiler parameters: always provide PolyML.Compiler.CPDebug, ignore global default; tuned;

report possible breakpoint positions;

proper attribute;

forgotten selector

made code less loopy

keep smart default for Isar proofs in Sledgehammer panel (if the option is not checked)

generalized generic translation function

merge

tuning

generalized limitation in documentation

made tactic more robust w.r.t. equations containing 'case_prod'

merged

merged

clarified boundary cases of completion;

additional ML parse tree components for Poly/ML 5.5.3, or later; support for ML completion; tuned;

added option ML_debugger;

ML debugger interface;

{r,e,d,f}tac with proper context in BNF

move disjoint sets to their own theory

back to uniform BUILD_ARGS: first some options, then some sessions (cf. 4fce5d462afc);

merged

more explicit command-line option for isabelle build;

more aggressive compaction of multi-goal proof terms (see also a8babbb6d5ea, 4dd0ba632e40);