NEWS
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;
2008-06-28 wenzelm 2008-06-28 ML: improved antiquotations;
2008-06-23 wenzelm 2008-06-23 induct_tac: mutual rules work as for method "induct";
2008-06-20 haftmann 2008-06-20 (removed non-present change)
2008-06-19 wenzelm 2008-06-19 disposed Sign.read_typ etc;
2008-06-18 wenzelm 2008-06-18 * Disposed old term read functions;
2008-06-16 wenzelm 2008-06-16 * Rules and tactics that read instantiations now demand a proper context;
2008-06-14 wenzelm 2008-06-14 removed exotic 'token_translation' command;
2008-06-13 wenzelm 2008-06-13 * Recovered hiding of consts;
2008-06-11 wenzelm 2008-06-11 tuned;
2008-06-10 wenzelm 2008-06-10 tuned spacing;
2008-06-10 wenzelm 2008-06-10 * Attributes cases, induct, coinduct support del option.
2008-06-10 wenzelm 2008-06-10 proper news header; methods case_tac and induct_tac now refer to usual declarations; removed obsolete induct_tac and thm_induct_tac;
2008-06-10 haftmann 2008-06-10 rep_datatype command now takes list of constructors as input arguments
2008-06-03 wenzelm 2008-06-03 some reorganization and fine-tuning;
2008-06-03 wenzelm 2008-06-03 reorganized isar-ref;
2008-05-28 wenzelm 2008-05-28 misc tuning for Isabelle2008;
2008-05-21 berghofe 2008-05-21 Added entry explaining incompatibilities introduced by replacing sets by predicates.
2008-05-18 wenzelm 2008-05-18 * Eliminated theory ProtoPure and CPure, leaving just one Pure theory.
2008-05-16 wenzelm 2008-05-16 * Method "cases", "induct", "coinduct": removed obsolete "(open)" option; * Isar statements: removed obsolete case "rule_context";
2008-05-15 wenzelm 2008-05-15 tuned;
2008-05-15 wenzelm 2008-05-15 * Simplified pdfsetup.sty;
2008-05-13 krauss 2008-05-13 NEWS about measure functions
2008-05-12 wenzelm 2008-05-12 misc tuning;
2008-05-02 ballarin 2008-05-02 unfold_locales part of default method.
2008-04-29 haftmann 2008-04-29 added lemma antiquotation
2008-04-25 krauss 2008-04-25 Merged theories about wellfoundedness into one: Wellfounded.thy
2008-04-19 wenzelm 2008-04-19 NamedThmsFun: removed obsolete print command -- facts are accesible via dynamic name;
2008-04-17 wenzelm 2008-04-17 * Context-dependent token translations.
2008-04-16 berghofe 2008-04-16 Added entry for unused_thms command.
2008-04-15 wenzelm 2008-04-15 added hide fact;
2008-04-15 wenzelm 2008-04-15 tuned;
2008-04-15 wenzelm 2008-04-15 * Name space merge now observes canonical order; * Authentic naming of facts;
2008-04-08 wenzelm 2008-04-08 support for YXML notation -- XML done right;
2008-04-07 paulson 2008-04-07 * Metis: the maximum number of clauses that can be produced from a theorem is now given by the attribute max_clauses. Theorems that exceed this number are ignored, with a warning printed.
2008-04-02 haftmann 2008-04-02 explicit class "eq" for operational equality