NEWS
2008-03-19 ago removed redundant Nat.less_not_sym, Nat.less_asym;
2008-03-19 ago Attributes sledgehammer_full, sledgehammer_modulus, sledgehammer_sorts
2008-03-18 ago theory loader: discontinued *attached* ML scripts;
2008-03-18 ago removed redundant less_trans, less_linear, le_imp_less_or_eq, le_less_trans, less_le_trans (cf. Orderings.thy);
2008-03-07 ago added entries
2008-03-06 ago * system/system_out provides a robust way to invoke external shell
2008-03-06 ago removed obsolete THIS_IS_ISABELLE_BUILD;
2008-03-05 ago indexing literal facts: exclude background context;
2008-03-05 ago NEWS: RBTs, renamings in ZF
2008-03-01 ago added @{const} antiquotation;
2008-02-28 ago Transitive_Closure: induct and cases rules now declare proper case_names;
2008-02-26 ago added accidental omissions
2008-02-17 ago New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
2008-02-15 ago <= and < on nat no longer depend on wellfounded relations
2008-02-06 ago 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 ago Theorem Inductive.lfp_ordinal_induct generalized to complete lattices
2008-01-28 ago * Outer syntax: string tokens no longer admit escaped white space;
2008-01-27 ago use_thy: do not set implicit ML context anymore;
2008-01-25 ago tuned;
2008-01-25 ago * Default settings: PROOFGENERAL_OPTIONS no longer impose xemacs here;
2008-01-25 ago moved definition of power on ints to theory Int
2008-01-22 ago added class semiring_div
2008-01-15 ago joined theories IntDef, Numeral, IntArith to theory Int
2008-01-14 ago *** empty log message ***
2008-01-06 ago * Rudimentary Isabelle plugin for jEdit;
2008-01-02 ago tuned;
2008-01-02 ago Multithreading.max_threads := 0 refers to number of cores of underlying machine;
2008-01-02 ago split of class uminus
2007-12-20 ago ``print mode'' is now a thread-local value derived from a global template;
2007-12-20 ago * Metis prover an order of magnitude faster, works with multithreading.
2007-12-19 ago instantiation target
2007-12-19 ago replaced K_record by lambda term %x. c
2007-12-17 ago spread NEWS about "induction_scheme" method
2007-12-15 ago tuned;
2007-12-15 ago * isatool browser now works with Cygwin;
2007-12-14 ago * isatool tty runs Isabelle process with plain tty interaction;
2007-12-12 ago tuned
2007-12-11 ago tuned
2007-12-07 ago (alt)string: allow explicit character codes (as in ML);
2007-12-06 ago added new primrec package
2007-12-04 ago \<chi> is now considered a letter;
2007-11-30 ago adjustions to due to instance target
2007-11-30 ago *** empty log message ***
2007-11-29 ago instance command as rudimentary class target
2007-11-26 ago moved new NEWS from Isabelle2007 to this Isabelle version'';
2007-11-23 ago deleted card definition as code lemma; authentic syntax for card
2007-11-20 ago tuned spacing;
2007-11-15 ago cover ISABELLE_IDENTIFIER;
2007-11-13 ago tuned;
2007-11-12 ago fixed typo;
2007-11-11 ago * HOL-Statespace;
2007-10-26 ago tuned
2007-10-26 ago added NEWS entry for function package
2007-10-25 ago tuned
2007-10-24 ago tuned file names etc.;
2007-10-24 ago tuned
2007-10-22 ago tuned Nominal entry;
2007-10-22 ago added @{sort}, @{type_syntax} antiquotations;
2007-10-21 ago misc tuning;
2007-10-21 ago tuned the entry about nominal datatypes