prefer explicit Keyword.keywords;

simplified keyword kinds; more explicit bootstrap syntax;

Tidying up. Removing unnecessary conditions from some theorems.

more complete fp_sugars for sum and prod; tuned; removed theorem duplicates; removed obsolete Lifting_{Option,Product,Sum} theories

document '*_transfer' attribute

document 'size_neq'

generate 'size_neq' for datatypes

fix 'unfla' function

proper oriented equivalence of dvd predicate and mod

merged

more symbols;

tuned signature;

more uniform header_keywords in ML/Scala; tuned signature;

tuned;

more frugal keywords;

eliminated pointless dynamic keywords (TTY legacy);

explicit type Keyword.keywords; tuned signature;

tuned;

clarified representation of type Keywords; tuned signature;

explicit type Keyword.Keywords;

clarified minor/major lexicon (like ML version);

reduced execution time

proper button margins for Nimbus L&F; properties are sorted when saved;

approximative update of versions;

Added Option.bind_split{,_asm,s}

clarified legacy code;

eliminated unused int_only flag (see also c12484a27367); just proper commands;

eliminated obsolete Proof.goal_message -- print outcome more directly;

updated to scala-2.11.4;

less ambitious isatest: polyml-5.3.0 has problems with big sessions like HOL-Proofs;

modernized header uniformly as section;

prefer \setisabellecontext;

modernized header;

modernized header;

obsolete;

modernized header;

obsolete;

modernized header;

modernized header;

modernized header;

modernized header;

modernized header;

modernized header;

modernized header;

clarified legacy command;

modernized header;

obsolete;

added update_header tool;

modernized header;

more flexibile \setisabellecontext, independently of header;

prefer explicit heading command;

uniform heading commands work in any context, even in theory header; discontinued obsolete 'sect', 'subsect', 'subsubsect'; marked obsolete 'header' as legacy;

eliminated dead code;

clarified syntax -- avoid overlap with command category;

tuned signature (see ab2483fad861);

recover via scanner; tuned signature;

simplified -- scanning is never interactive;

tuned signature, in accordance to Scala version;

command-line terminator ";" is no longer accepted;

eliminated spurious semicolons;

eliminated former Proof General preferences;

merged

tuned;

provide explicit theory (amending 621c052789b4);

removed pointless markup; tuned comments;

discontinued obsolete \<^sync> marker;

discontinued obsolete control command category;

obsolete;

obsolete;

discontinued obsolete tty and prompt;

discontinued pointless option: timing is always on (overall theory only);

eliminated odd flags and hook;

avoid noise (cf. 03ff4d1e6784);

discontinued Isar TTY loop;

removed obsolete Proof General commands;

obsolete;

discontinued obsolete Output.urgent_message;

discontinued Proof General;

Some comments and a new version of a result

merged

eliminated aliases;

eliminated aliases;

eliminated aliases;

tuned spelling;

hardwired imitation of copy.shortcut2 default;

more simp rules concerning dvd and even/odd

choose_reduce_nat: re-ordered operands

make SML/NJ more happy;

proper syntax categery "name" -- as usual and as documented;

disable coercions for NO_MATCH

merged

modernized setup;

merged

modernized setup;

modernized setup;

modernized setup;

modernized setup;

modernized setup;

modernized setup;

modernized setup;

modernized setup; tuned whitespace;

modernized setup;

modernized setup;

modernized setup; more standard module name;

modernized setup;

modernized setup; tuned whitespace;

tuned;

modernized setup;

modernized setup; more standard module name;

more standard theory name;

more iterators;

removed useless lemmas

tuned layout and proofs

tuned proofs; tuned white space; more symbols;

increase chances that HOL-Proofs image still works for polyml-5.3.0;

tuned signature;

proper selectMatch, e.g. relevant for S-click on gutter;

find command span in buffer; tuned signature;

'notepad' requires proper nesting of begin/end;

explicit keyword category for commands that may start a block;