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