NEWS
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
2008-03-30 nipkow 2008-03-30 *** empty log message ***
2008-03-29 wenzelm 2008-03-29 purely functional setup of claset/simpset/clasimpset;
2008-03-29 wenzelm 2008-03-29 fixed spelling;
2008-03-29 wenzelm 2008-03-29 * Eliminated destructive theorem database. * Commands 'use' and 'ML' are now purely functional; added diagnostic 'ML_val'.
2008-03-27 haftmann 2008-03-27 explicit case names for rule list_induct2
2008-03-27 wenzelm 2008-03-27 Command 'setup': discontinued implicit version.
2008-03-27 wenzelm 2008-03-27 HOL (and FOL): renamed variables in rules imp_elim and swap; Eliminated theory ProtoPure.
2008-03-25 wenzelm 2008-03-25 Functor NamedThmsFun: data is available to the user as dynamic fact;
2008-03-24 wenzelm 2008-03-24 removed obsolete use_legacy_bindings;
2008-03-20 haftmann 2008-03-20 Theory Product_Type; fixed typos
2008-03-19 wenzelm 2008-03-19 removed redundant Nat.less_not_sym, Nat.less_asym; renamed Nat.less_irrefl to less_irrefl_nat, no longer declared elim;
2008-03-19 paulson 2008-03-19 Attributes sledgehammer_full, sledgehammer_modulus, sledgehammer_sorts Sledgehammer no longer produces structured proofs by default.
2008-03-18 wenzelm 2008-03-18 theory loader: discontinued *attached* ML scripts;
2008-03-18 wenzelm 2008-03-18 removed redundant less_trans, less_linear, le_imp_less_or_eq, le_less_trans, less_le_trans (cf. Orderings.thy); renamed less_imp_le to less_imp_le_nat;
2008-03-07 haftmann 2008-03-07 added entries
2008-03-06 wenzelm 2008-03-06 * system/system_out provides a robust way to invoke external shell commands, with propagation of interrupts (after Poly/ML 5.2);
2008-03-06 wenzelm 2008-03-06 removed obsolete THIS_IS_ISABELLE_BUILD;
2008-03-05 wenzelm 2008-03-05 indexing literal facts: exclude background context;
2008-03-05 krauss 2008-03-05 NEWS: RBTs, renamings in ZF
2008-03-01 wenzelm 2008-03-01 added @{const} antiquotation;
2008-02-28 wenzelm 2008-02-28 Transitive_Closure: induct and cases rules now declare proper case_names; tuned;
2008-02-26 haftmann 2008-02-26 added accidental omissions
2008-02-17 huffman 2008-02-17 New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
2008-02-15 haftmann 2008-02-15 <= and < on nat no longer depend on wellfounded relations
2008-02-06 haftmann 2008-02-06 locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
2008-01-30 haftmann 2008-01-30 Theorem Inductive.lfp_ordinal_induct generalized to complete lattices
2008-01-28 wenzelm 2008-01-28 * Outer syntax: string tokens no longer admit escaped white space;
2008-01-27 wenzelm 2008-01-27 use_thy: do not set implicit ML context anymore;
2008-01-25 wenzelm 2008-01-25 tuned;
2008-01-25 wenzelm 2008-01-25 * Default settings: PROOFGENERAL_OPTIONS no longer impose xemacs here;
2008-01-25 haftmann 2008-01-25 moved definition of power on ints to theory Int
2008-01-22 haftmann 2008-01-22 added class semiring_div
2008-01-15 haftmann 2008-01-15 joined theories IntDef, Numeral, IntArith to theory Int
2008-01-14 nipkow 2008-01-14 *** empty log message ***
2008-01-06 wenzelm 2008-01-06 * Rudimentary Isabelle plugin for jEdit;
2008-01-02 wenzelm 2008-01-02 tuned;
2008-01-02 wenzelm 2008-01-02 Multithreading.max_threads := 0 refers to number of cores of underlying machine;
2008-01-02 haftmann 2008-01-02 split of class uminus
2007-12-20 wenzelm 2007-12-20 ``print mode'' is now a thread-local value derived from a global template;
2007-12-20 wenzelm 2007-12-20 * Metis prover an order of magnitude faster, works with multithreading.
2007-12-19 haftmann 2007-12-19 instantiation target
2007-12-19 schirmer 2007-12-19 replaced K_record by lambda term %x. c