NEWS
2005-11-10 wenzelm 2005-11-10 renamed Thm.cgoal_of to Thm.cprem_of;
2005-10-31 haftmann 2005-10-31 nth_*, fold_index refined
2005-10-28 wenzelm 2005-10-28 tuned;
2005-10-28 wenzelm 2005-10-28 * Pure/Isar: literal facts; * ML/Pure: tuned Thm.lift_rule; * ML/Pure: renamed Goal constant to prop, more general uses;
2005-10-27 wenzelm 2005-10-27 * HOL: alternative iff syntax;
2005-10-27 haftmann 2005-10-27 added module Pure/General/rat.ML
2005-10-21 wenzelm 2005-10-21 * Legacy goal package: reduced interface to the bare minimum required to keep existing proof scripts running. * Internal goals: structure Goal.
2005-10-19 wenzelm 2005-10-19 * Theory syntax: discontinued non-Isar format and old Isar headers;
2005-10-18 wenzelm 2005-10-18 Simplifier.context/theory_context;
2005-10-17 wenzelm 2005-10-17 * Simplifier: simpset of a running simplification process contains a proof context; * Simplifier.inherit_context supercedes Simplifier.inherit_bounds; * Simplifier/Classical Reasoner: more abstract interfaces change_simpset/claset;
2005-10-17 wenzelm 2005-10-17 tuned;
2005-10-15 wenzelm 2005-10-15 tuned;
2005-10-15 wenzelm 2005-10-15 * antiquotations ML_type, ML_struct; * Isar 'guess' element;
2005-10-09 webertj 2005-10-09 Tactics sat and satx reimplemented, several improvements
2005-10-08 nipkow 2005-10-08 *** empty log message ***
2005-10-07 wenzelm 2005-10-07 tuned;
2005-10-07 wenzelm 2005-10-07 added dummy variable binding; removed obsolete _K;
2005-10-04 wenzelm 2005-10-04 * Command 'find_theorems': support * wildcard in name: criterion.
2005-09-29 wenzelm 2005-09-29 pdfsetup.sty: better not rely on ifpdf.sty;
2005-09-29 wenzelm 2005-09-29 Isabelle2005 (October 2005); pdfsetup.sty now requires ifpdf.sty; added Simplifier.debug_bounds; do not advertize Simplifier.add_context_simprocs etc., which are to be replaced soon;
2005-09-29 wenzelm 2005-09-29 tuned;
2005-09-28 webertj 2005-09-28 pointer to HOL/ex/SAT_Examples.thy added
2005-09-28 wenzelm 2005-09-28 revert 'defs' advertisement; removed PG/xemacs note, which is actually wrong now; tuned;
2005-09-27 wenzelm 2005-09-27 more details about incomplete 'defs';
2005-09-27 wenzelm 2005-09-27 tuned;
2005-09-27 berghofe 2005-09-27 Added entries for code_module, code_library, and value.
2005-09-25 wenzelm 2005-09-25 * Hyperreal: A theory of Taylor series.
2005-09-23 webertj 2005-09-23 new sat tactic
2005-09-23 wenzelm 2005-09-23 tuned;
2005-09-23 paulson 2005-09-23 ATP linkup
2005-09-23 nipkow 2005-09-23 *** empty log message ***
2005-09-22 huffman 2005-09-22 HOLCF theorem naming conventions
2005-09-21 haftmann 2005-09-21 added AList.make, eq_fst, apr ...
2005-09-21 wenzelm 2005-09-21 tunes;
2005-09-21 wenzelm 2005-09-21 tuned;
2005-09-20 wenzelm 2005-09-20 tuned;
2005-09-20 wenzelm 2005-09-20 tuned;
2005-09-20 wenzelm 2005-09-20 HOL/ex/Chinese.thy; PROOFGENERAL_OPTIONS: no longer prefer xemacs;
2005-09-20 haftmann 2005-09-20 infix operator precedence
2005-09-17 wenzelm 2005-09-17 HTML.with_charset;
2005-09-17 wenzelm 2005-09-17 Cube: converted to Isar, use locales;
2005-09-16 huffman 2005-09-16 add HOLCF entries for pcpodef, cont_proc, fixrec; add HOL-Complex entry for transfer tactic; clean up lists of theories in HOL-Complex entries
2005-09-16 ballarin 2005-09-16 tuned
2005-09-15 wenzelm 2005-09-15 * Improved efficiency of the Simplifier etc.;
2005-09-15 wenzelm 2005-09-15 incorporated HOL/Hyperreal/CHANGES;
2005-09-15 wenzelm 2005-09-15 command 'thms_containing' has been discontinued in favour of 'find_theorems'; TableFun/Symtab: curried lookup and update; tuned;
2005-09-15 haftmann 2005-09-15 AList, the_*
2005-09-14 wenzelm 2005-09-14 tuned;
2005-09-14 wenzelm 2005-09-14 hide: added option '(open)';
2005-09-14 schirmer 2005-09-14 ... prem19
2005-09-14 wenzelm 2005-09-14 Method comm_ring for proving equalities in commutative rings.
2005-09-14 wenzelm 2005-09-14 HOL: method comm_ring; Proof General: Unicode (UTF-8) support;
2005-09-13 wenzelm 2005-09-13 tuned;
2005-09-06 wenzelm 2005-09-06 axclass: name space prefix is now "c_class" instead of just "c"; typedef: proper support for polymorphic sets;
2005-09-05 wenzelm 2005-09-05 tuned;
2005-09-05 wenzelm 2005-09-05 Markup commands 'chapter' .. 'text' support optional locale specification;
2005-09-02 ballarin 2005-09-02 print_locale omits facts by default
2005-08-31 wenzelm 2005-08-31 * Delimiters of outer tokens now produce separate LaTeX macros; * isatool usedir: option -C (default true) controls copying of document directory;
2005-08-30 paulson 2005-08-30 patterns in setsum and setprod
2005-08-28 wenzelm 2005-08-28 * ML functions legacy_bindings and use_legacy_bindings;