NEWS
2008-11-20 wenzelm 2008-11-20 Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
2008-11-19 nipkow 2008-11-19 *** empty log message ***
2008-11-13 haftmann 2008-11-13 simproc for let
2008-10-30 ballarin 2008-10-30 Dropped context element 'includes'.
2008-10-28 paulson 2008-10-28 The metis method no longer fails because the theorem is too trivial
2008-10-24 haftmann 2008-10-24 new classes "top" and "bot"
2008-10-23 wenzelm 2008-10-23 multithreading support only for polyml-5.2.1 or later;
2008-10-16 wenzelm 2008-10-16 tuned;
2008-10-16 wenzelm 2008-10-16 tuned;
2008-10-16 wenzelm 2008-10-16 goal-directed proof now enforces strict proof irrelevance wrt. sort hypotheses;
2008-10-15 wenzelm 2008-10-15 tuned;
2008-10-15 wenzelm 2008-10-15 tuned;
2008-10-15 wenzelm 2008-10-15 generic ATP manager based on threads (by Fabian Immler);
2008-10-10 haftmann 2008-10-10 tuned
2008-10-10 haftmann 2008-10-10 tuned default rules of (dvd)
2008-10-07 haftmann 2008-10-07 only one theorem table for both code generators
2008-10-04 wenzelm 2008-10-04 simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
2008-10-03 wenzelm 2008-10-03 tuned;
2008-10-03 wenzelm 2008-10-03 Vampire wrapper script for remote SystemOnTPTP service (by Fabian Immler);
2008-09-25 haftmann 2008-09-25 non left-linear equations for nbe
2008-09-18 wenzelm 2008-09-18 tuned;
2008-09-18 wenzelm 2008-09-18 simplified oracle interface;
2008-09-17 wenzelm 2008-09-17 * ML bindings produced via Isar commands are stored within the Isar context. * Command 'ML_prf' is analogous to 'ML' but works within a proof context.
2008-09-16 wenzelm 2008-09-16 multithreading for Poly/ML 5.1 is no longer supported;
2008-09-16 wenzelm 2008-09-16 updated system manual;
2008-09-16 wenzelm 2008-09-16 separate emacs tool for Proof General / Emacs;
2008-09-16 paulson 2008-09-16 The metis method now fails in the usual manner, rather than raising an exception, if it determines that it cannot prove the theorem.
2008-09-16 haftmann 2008-09-16 generic value command
2008-09-09 wenzelm 2008-09-09 * Changed defaults for unify configuration options;
2008-09-05 haftmann 2008-09-05 different bookkeeping for code equations
2008-09-03 wenzelm 2008-09-03 axiomatization is now global-only;
2008-09-03 wenzelm 2008-09-03 simplified Toplevel.add_hook: cover successful transactions only;
2008-09-02 wenzelm 2008-09-02 * Generic Toplevel.add_hook interface allows to analyze the result of transactions (including failed ones). For example, see src/Pure/ProofGeneral/proof_general_pgip.ML for theorem dependency output of transactions resulting in a new theory state.
2008-09-02 wenzelm 2008-09-02 * Result facts now refer to the *full* internal name;
2008-09-02 wenzelm 2008-09-02 * Name bindings in higher specification mechanisms;
2008-09-02 ballarin 2008-09-02 Interpretation commands no longer accept interpretation attributes.
2008-09-01 nipkow 2008-09-01 *** empty log message ***
2008-08-29 haftmann 2008-08-29 dropped parameter prefix for class theorems
2008-08-23 wenzelm 2008-08-23 * Isabelle/lib/classes/Pure.jar; * Status messages; * Homegrown Isabelle font;
2008-08-11 haftmann 2008-08-11 moved class wellorder to theory Orderings
2008-08-08 wenzelm 2008-08-08 tuned formatting;
2008-08-06 ballarin 2008-08-06 Interpretation command (theory/proof context) no longer simplifies goal.
2008-08-01 ballarin 2008-08-01 Generalised polynomial lemmas from cring to ring.
2008-07-30 ballarin 2008-07-30 New locales for orders and lattices where the equivalence relation is not restricted to equality.
2008-07-29 ballarin 2008-07-29 Zorn's Lemma for partial orders.
2008-07-29 ballarin 2008-07-29 Unit_inv_l, Unit_inv_r made [simp]; Renamed theorems; New theory on divisibility.
2008-07-25 haftmann 2008-07-25 dropped locale (open)
2008-07-18 haftmann 2008-07-18 moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
2008-07-15 wenzelm 2008-07-15 added command 'linear_undo'; tuned;
2008-07-14 haftmann 2008-07-14 unified curried gcd, lcm, zgcd, zlcm
2008-07-11 haftmann 2008-07-11 Fract now total; improved code generator setup
2008-07-10 wenzelm 2008-07-10 slightly improved @{lemma} (both for latex and ML); misc tuning;
2008-07-04 huffman 2008-07-04 HOL-NSA
2008-07-02 haftmann 2008-07-02 code antiquotation roaring ahead
2008-07-01 haftmann 2008-07-01 HOL += HOL-Complex
2008-07-01 haftmann 2008-07-01 HOL += HOL-Complex
2008-06-28 wenzelm 2008-06-28 tuned;
2008-06-28 wenzelm 2008-06-28 tuned;
2008-06-28 wenzelm 2008-06-28 additional ML antiquotations;
2008-06-28 wenzelm 2008-06-28 @{lemma}: 'by' keyword;