NEWS
2005-12-23 wenzelm 2005-12-23 tuned;
2005-12-23 wenzelm 2005-12-23 * Provers/induct: support simultaneous goals with mutual rules;
2005-12-23 haftmann 2005-12-23 is_prefix
2005-12-22 wenzelm 2005-12-22 tuned;
2005-12-22 wenzelm 2005-12-22 * induct: improved treatment of mutual goals and mutual rules;
2005-12-21 haftmann 2005-12-21 discontinued unflat in favour of burrow and burrow_split
2005-12-20 wenzelm 2005-12-20 tuned;
2005-12-16 haftmann 2005-12-16 re-arranged tuples (theory * 'a) to ('a * theory) in Pure
2005-12-13 wenzelm 2005-12-13 Provers/induct: coinduct; HOL/Library: theory Coinductive_List;
2005-12-08 wenzelm 2005-12-08 removed hint for Classical.swap, which is not really user-level anyway;
2005-12-08 wenzelm 2005-12-08 * HOL: Theorem 'swap' is no longer bound at the ML top-level.
2005-11-30 wenzelm 2005-11-30 simulaneous 'def';
2005-11-27 wenzelm 2005-11-27 * Provers/induct: obtain pattern;
2005-11-25 wenzelm 2005-11-25 tuned;
2005-11-23 wenzelm 2005-11-23 tuned;
2005-11-23 wenzelm 2005-11-23 Provers/induct: definitional insts and fixing;
2005-11-23 wenzelm 2005-11-23 tuned;
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