2016-04-02 ago wenzelm tuned;
2016-04-02 ago wenzelm tuned signature;
2016-04-02 ago wenzelm proper type;
2016-04-02 ago wenzelm careful export of type-dependent functions, without losing their special status;
2016-04-02 ago wenzelm clarified modules;
2016-04-02 ago wenzelm clarified modules;
2016-04-02 ago blanchet tuned LaTeX
2016-04-02 ago blanchet import package that might help on some machines (e.g., macbroy2)
2016-04-02 ago wenzelm clarified check_sources;
2016-04-02 ago wenzelm obsolete (see 1d977436c1bf);
2016-04-02 ago wenzelm more robust display of bidirectional Unicode text: enforce left-to-right;
2016-04-01 ago wenzelm merged
2016-04-01 ago wenzelm merged
2016-04-01 ago wenzelm explicit warning about bidi uncertainty in Unicode;
2016-04-01 ago wenzelm explicit warning about formal use of Unicode;
2016-04-01 ago wenzelm documentation;
2016-04-01 ago wenzelm more markup;
2016-04-01 ago wenzelm require actual space;
2016-04-01 ago wenzelm tuned signature;
2016-04-01 ago wenzelm required space is already part of Position.here;
2016-04-01 ago wenzelm tuned messages;
2016-04-01 ago wenzelm clarified errors -- disallow cartouche fragments as delimiter;
2016-04-01 ago wenzelm tuned signature;
2016-04-01 ago wenzelm tuned;
2016-04-01 ago wenzelm clarified end position;
2016-04-01 ago wenzelm tuned signature;
2016-04-01 ago wenzelm tuned;
2016-04-01 ago wenzelm removed redundant Position.set_range -- already done in Position.range;
2016-04-01 ago wenzelm lower threshold -- command timing for proofs is cumulative, e.g. HOL 672 ~> 8889;
2016-04-01 ago wenzelm less bulky timing information, e.g. HOL 56913 ~> 672;
2016-04-01 ago wenzelm tuned;
2016-04-01 ago wenzelm more operations (cf. Scala version);
2016-04-01 ago wenzelm tuned whitespace;
2016-04-01 ago wenzelm explicit property for unbreakable block;
2016-04-01 ago wenzelm unused;
2016-04-01 ago wenzelm tuned markup;
2016-04-01 ago wenzelm clarified treatment of properties;
2016-04-01 ago wenzelm more robust pretty printing: permissive treatment of bad values;
2016-04-01 ago wenzelm adapted to Poly/ML repository version 2e40cadc975a;
2016-03-31 ago wenzelm explicit mixfix block properties;
2016-03-31 ago wenzelm clarified modules;
2016-03-31 ago wenzelm tuned signature;
2016-04-01 ago blanchet reintroduced check that may guard some tactic failures
2016-04-01 ago blanchet adapt theory names within the theory
2016-03-31 ago traytel made tactic more robust
2016-03-31 ago traytel tuned interface
2016-03-30 ago wenzelm merged
2016-03-30 ago wenzelm proper object-logic constraint (amending dd2914250ca7);
2016-03-30 ago wenzelm reconcile object-logic constraint vs. mixfix constraint;
2016-03-30 ago wenzelm more explicit support for object-logic constraint;
2016-03-30 ago wenzelm more language markup;
2016-03-30 ago wenzelm more accurate mixfix type constraints;
2016-03-30 ago wenzelm tuned;
2016-03-30 ago wenzelm tuned message;
2016-03-30 ago wenzelm more explicit type;
2016-03-30 ago wenzelm relevant check_mixfix happens further at the bottom, to avoid duplicate reports via Specification.prepare;
2016-03-30 ago wenzelm avoid duplicate reports;
2016-03-30 ago wenzelm tuned messages -- position is usually missing here;
2016-03-30 ago wenzelm more PIDE markup;
2016-03-30 ago wenzelm clarified modules;