NEWS
Mon, 17 Oct 2005 23:10:25 +0200 wenzelm * Simplifier: simpset of a running simplification process contains a proof context;
Mon, 17 Oct 2005 23:10:16 +0200 wenzelm tuned;
Sat, 15 Oct 2005 00:14:30 +0200 wenzelm tuned;
Sat, 15 Oct 2005 00:08:14 +0200 wenzelm * antiquotations ML_type, ML_struct;
Sun, 09 Oct 2005 17:06:03 +0200 webertj Tactics sat and satx reimplemented, several improvements
Sat, 08 Oct 2005 23:36:01 +0200 nipkow *** empty log message ***
Fri, 07 Oct 2005 22:59:17 +0200 wenzelm tuned;
Fri, 07 Oct 2005 22:59:15 +0200 wenzelm added dummy variable binding;
Tue, 04 Oct 2005 16:47:39 +0200 wenzelm * Command 'find_theorems': support * wildcard in name: criterion.
Thu, 29 Sep 2005 17:08:52 +0200 wenzelm pdfsetup.sty: better not rely on ifpdf.sty;
Thu, 29 Sep 2005 15:50:43 +0200 wenzelm Isabelle2005 (October 2005);
Thu, 29 Sep 2005 00:58:54 +0200 wenzelm tuned;
Wed, 28 Sep 2005 18:50:42 +0200 webertj pointer to HOL/ex/SAT_Examples.thy added
Wed, 28 Sep 2005 11:50:13 +0200 wenzelm revert 'defs' advertisement;
Tue, 27 Sep 2005 17:24:27 +0200 wenzelm more details about incomplete 'defs';
Tue, 27 Sep 2005 11:27:07 +0200 wenzelm tuned;
Tue, 27 Sep 2005 11:03:38 +0200 berghofe Added entries for code_module, code_library, and value.
Sun, 25 Sep 2005 20:24:23 +0200 wenzelm * Hyperreal: A theory of Taylor series.
Fri, 23 Sep 2005 23:28:59 +0200 webertj new sat tactic
Fri, 23 Sep 2005 13:20:47 +0200 wenzelm tuned;
Fri, 23 Sep 2005 10:25:55 +0200 paulson ATP linkup
Fri, 23 Sep 2005 00:10:58 +0200 nipkow *** empty log message ***
Thu, 22 Sep 2005 18:59:41 +0200 huffman HOLCF theorem naming conventions
Wed, 21 Sep 2005 17:21:35 +0200 haftmann added AList.make, eq_fst, apr ...
Wed, 21 Sep 2005 11:50:52 +0200 wenzelm tunes;
Wed, 21 Sep 2005 00:07:32 +0200 wenzelm tuned;
Tue, 20 Sep 2005 22:02:06 +0200 wenzelm tuned;
Tue, 20 Sep 2005 21:48:47 +0200 wenzelm tuned;
Tue, 20 Sep 2005 14:20:58 +0200 wenzelm HOL/ex/Chinese.thy;
Tue, 20 Sep 2005 08:20:22 +0200 haftmann infix operator precedence
Sat, 17 Sep 2005 18:11:17 +0200 wenzelm HTML.with_charset;
Sat, 17 Sep 2005 12:18:00 +0200 wenzelm Cube: converted to Isar, use locales;
Fri, 16 Sep 2005 23:55:23 +0200 huffman add HOLCF entries for pcpodef, cont_proc, fixrec;
Fri, 16 Sep 2005 14:44:52 +0200 ballarin tuned
Thu, 15 Sep 2005 20:27:48 +0200 wenzelm * Improved efficiency of the Simplifier etc.;
Thu, 15 Sep 2005 20:24:53 +0200 wenzelm incorporated HOL/Hyperreal/CHANGES;
Thu, 15 Sep 2005 17:16:53 +0200 wenzelm command 'thms_containing' has been discontinued in favour of 'find_theorems';
Thu, 15 Sep 2005 10:00:01 +0200 haftmann AList, the_*
Wed, 14 Sep 2005 23:31:09 +0200 wenzelm tuned;
Wed, 14 Sep 2005 23:15:00 +0200 wenzelm hide: added option '(open)';
Wed, 14 Sep 2005 23:06:02 +0200 schirmer ... prem19
Wed, 14 Sep 2005 22:18:55 +0200 wenzelm Method comm_ring for proving equalities in commutative rings.
Wed, 14 Sep 2005 22:04:36 +0200 wenzelm HOL: method comm_ring;
Tue, 13 Sep 2005 22:49:12 +0200 wenzelm tuned;
Tue, 06 Sep 2005 16:59:50 +0200 wenzelm axclass: name space prefix is now "c_class" instead of just "c";
Mon, 05 Sep 2005 17:49:28 +0200 wenzelm tuned;
Mon, 05 Sep 2005 17:38:15 +0200 wenzelm Markup commands 'chapter' .. 'text' support optional locale specification;
Fri, 02 Sep 2005 09:50:58 +0200 ballarin print_locale omits facts by default
Wed, 31 Aug 2005 15:46:30 +0200 wenzelm * Delimiters of outer tokens now produce separate LaTeX macros;
Tue, 30 Aug 2005 12:47:53 +0200 paulson patterns in setsum and setprod
Sun, 28 Aug 2005 16:06:07 +0200 wenzelm * ML functions legacy_bindings and use_legacy_bindings;
Sun, 28 Aug 2005 16:04:50 +0200 wenzelm tuned;
Wed, 24 Aug 2005 12:07:00 +0200 ballarin Printing of interpretations: option to show witness theorems;
Thu, 18 Aug 2005 11:59:17 +0200 wenzelm * The ML antiquotation prints type-checked ML expressions verbatim.
Thu, 18 Aug 2005 11:17:32 +0200 wenzelm * Proper output of proof terms within a proof context;
Wed, 17 Aug 2005 17:03:20 +0200 ballarin Interpretation in locales.
Wed, 17 Aug 2005 14:19:17 +0200 nipkow *** empty log message ***
Tue, 16 Aug 2005 13:42:13 +0200 wenzelm * Command tags control specific markup of certain regions of text (replaces usedir -H);
Wed, 03 Aug 2005 14:49:04 +0200 avigad mentioned change to exp_ge_add_one_self, new transitivity rules
Mon, 01 Aug 2005 19:21:38 +0200 wenzelm * Pure/Simplifier: improved handling of bound variables;
less more (0) -300 -100 -60 tip