tuned signature;

tuned;

removed redundant Position.set_range -- already done in Position.range;

lower threshold -- command timing for proofs is cumulative, e.g. HOL 672 ~> 8889;

less bulky timing information, e.g. HOL 56913 ~> 672;

tuned;

more operations (cf. Scala version);

tuned whitespace;

explicit property for unbreakable block;

unused;

tuned markup;

clarified treatment of properties; tuned messages;

more robust pretty printing: permissive treatment of bad values;

adapted to Poly/ML repository version 2e40cadc975a;

explicit mixfix block properties;

clarified modules;

tuned signature;

reintroduced check that may guard some tactic failures

adapt theory names within the theory

made tactic more robust

tuned interface

merged

proper object-logic constraint (amending dd2914250ca7);

reconcile object-logic constraint vs. mixfix constraint;

more explicit support for object-logic constraint;

more language markup;

more accurate mixfix type constraints;

tuned;

tuned message;

more explicit type; tuned;

relevant check_mixfix happens further at the bottom, to avoid duplicate reports via Specification.prepare;

avoid duplicate reports;