report final debugger_state more robustly, e.g. after interrupt;

eliminated global option: breakpoints control this individually;

more uniform ScrollPane, like graphview;

tuned signature; more rendering;

tuned rendering;

set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;

more thorough Encode.string;

added action to toggle breakpoints (on editor side);

sort lines;

rendering for debugger/breakpoint active state;

follow debugger focus;

tuned signature;

tuned imports;

tuned messages;

clarified ML options;

merged

more single stepping;

direct bootstrap of integer division from natural division

slight cleanup of lemmas

obsolete since no code generator without dictionary construction left

make SML/NJ work;

suppress empty messages as usual;

proper Symbol.decode/encode;

eval ML context; tuned GUI;

maintain history more often;

approximate old selection after update;

expand all rows for robustness and simplicity; tuned signature;

evaluate ML expressions within debugger context; redirected writeln/warning for ML compiler;

clarified debugger loop; more controls;

clarified thread state; support for eval operation;

tuned;

more controls;

tuned;

clarified signature, to make debugger.ML compile with current official ML versions;

support for tree selection;

proper dynamic update;

tuned;

more GUI components;

tuned;

tuned;

more controls;

proper initialization;

tuned signature;

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;