focus text field, to capture key events even on Mac OS X look-and-feel;

tuned proofs;

more tolerant treatment of end-of-buffer -- avoid debatable situations of jEdit buffer boundaries;

skip ignored commands, similar to former proper_command_at (see d68ea01d5084) -- relevant to Output, Query_Operation etc.; tuned signature;

clarified command spans (again, see also 03a2dc9e0624): restrict to proper range to allow Isabelle.command_edit adding material monotonically without destroying the command (e.g. relevant for sendback from sledgehammer); simplified command padding: always newline, despite lack of indentation;

tuned proofs;

obsolete;

tuned;

avoid clash of auto print functions with query operations, notably sledgehammer (cf. 3461985dcbc3);

tuned isatest options;

updated docs

added [dest] to "disc_exclude"

started adding support for "nat_case" as case study for all "case" constructs

temporary fix to tactic

made SML/NJ happy

tuning

support "of" syntax to disambiguate selector equations

don't note more induction principles than there are functions + tuning

more (co)data docs

improved rail diagram

use "primcorec" in example

use "primcorec" in doc

updated keywords

updated certificates

when "max_thm_instances" is hit, choose more carefully which instances should be kept

add "primcorec" command (cf. ae7f50e70c09)

merged

added lemmas

honor MaSh's zero-overhead policy -- no learning if the tool is disabled

adapted to reflect renaming of session