tuned;

tuned proofs;

prefer uniform Timing.message -- avoid assumption about sequential execution;

prefer final ADTs -- prevent ooddities;

more explicit Long_Name operations (NB: analyzing qualifiers is inherently fragile);

more standard settings -- refer to COMPONENT at most once;

clarified prems_lin_arith_tac, with subtle change of semantics: structured prems are inserted as well;

prefer cut_tac, where it is clear that the special variants cut_rules_tac or cut_facts_tac are not required;

eliminated odd comment from distant past;

updated cut_tac, without loose references to implementation manual;

updated generated file;

simplified cut_tac (cf. d549b5b0f344);

merged

avoid using constant Int.neg

reactivated Find_Unused_Assms_Examples to avoid untested / dead stuff in the repository; moved the whole HOL-Quickcheck_Examples target from "all" to "full" for now -- it does not terminate in certain situations (to be investigated further);

merged

added lemma

converting "set [...]" to "{...}" in evaluation results

removing Find_Unused_Assms_Examples from session as it requires much time

restored accidental omission

dropped dead code

tuned structure

retain syntax here

tuned structure; dropped already existing syntax declarations

tuned syntax declarations; tuned structure

merged

marked candidates for rule declarations

include warning messages in node status;

tuned signature (in accordance with ML);

more PIDE modules;

tuned proofs;

more abstract class Document.State;