NEWS
2008-10-16 ago tuned;
2008-10-16 ago tuned;
2008-10-16 ago goal-directed proof now enforces strict proof irrelevance wrt. sort hypotheses;
2008-10-15 ago tuned;
2008-10-15 ago tuned;
2008-10-15 ago generic ATP manager based on threads (by Fabian Immler);
2008-10-10 ago tuned
2008-10-10 ago tuned default rules of (dvd)
2008-10-07 ago only one theorem table for both code generators
2008-10-04 ago simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
2008-10-03 ago tuned;
2008-10-03 ago Vampire wrapper script for remote SystemOnTPTP service (by Fabian Immler);
2008-09-25 ago non left-linear equations for nbe
2008-09-18 ago tuned;
2008-09-18 ago simplified oracle interface;
2008-09-17 ago * ML bindings produced via Isar commands are stored within the Isar context.
2008-09-16 ago multithreading for Poly/ML 5.1 is no longer supported;
2008-09-16 ago updated system manual;
2008-09-16 ago separate emacs tool for Proof General / Emacs;
2008-09-16 ago The metis method now fails in the usual manner, rather than raising an exception,
2008-09-16 ago generic value command
2008-09-09 ago * Changed defaults for unify configuration options;
2008-09-05 ago different bookkeeping for code equations
2008-09-03 ago axiomatization is now global-only;
2008-09-03 ago simplified Toplevel.add_hook: cover successful transactions only;
2008-09-02 ago * Generic Toplevel.add_hook interface allows to analyze the result of
2008-09-02 ago * Result facts now refer to the *full* internal name;
2008-09-02 ago * Name bindings in higher specification mechanisms;
2008-09-02 ago Interpretation commands no longer accept interpretation attributes.
2008-09-01 ago *** empty log message ***
2008-08-29 ago dropped parameter prefix for class theorems
2008-08-23 ago * Isabelle/lib/classes/Pure.jar;
2008-08-11 ago moved class wellorder to theory Orderings
2008-08-08 ago tuned formatting;
2008-08-06 ago Interpretation command (theory/proof context) no longer simplifies goal.
2008-08-01 ago Generalised polynomial lemmas from cring to ring.
2008-07-30 ago New locales for orders and lattices where the equivalence relation is not restricted to equality.
2008-07-29 ago Zorn's Lemma for partial orders.
2008-07-29 ago Unit_inv_l, Unit_inv_r made [simp];
2008-07-25 ago dropped locale (open)
2008-07-18 ago moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
2008-07-15 ago added command 'linear_undo';
2008-07-14 ago unified curried gcd, lcm, zgcd, zlcm
2008-07-11 ago Fract now total; improved code generator setup
2008-07-10 ago slightly improved @{lemma} (both for latex and ML);
2008-07-04 ago HOL-NSA
2008-07-02 ago code antiquotation roaring ahead
2008-07-01 ago HOL += HOL-Complex
2008-07-01 ago HOL += HOL-Complex
2008-06-28 ago tuned;
2008-06-28 ago tuned;
2008-06-28 ago additional ML antiquotations;
2008-06-28 ago @{lemma}: 'by' keyword;
2008-06-28 ago ML: improved antiquotations;
2008-06-23 ago induct_tac: mutual rules work as for method "induct";
2008-06-20 ago (removed non-present change)
2008-06-19 ago disposed Sign.read_typ etc;
2008-06-18 ago * Disposed old term read functions;
2008-06-16 ago * Rules and tactics that read instantiations now demand a proper context;
2008-06-14 ago removed exotic 'token_translation' command;