NEWS
2006-01-15 ago tuned;
2006-01-15 ago tuned;
2006-01-15 ago * Classical: optional weight for attributes;
2006-01-14 ago tuned;
2006-01-14 ago * ML/Isar: simplified treatment of user-level errors;
2006-01-13 ago *** empty log message ***
2006-01-10 ago tuned;
2006-01-10 ago * ML: generic context, data, attributes;
2006-01-07 ago * Provers/induct: improved simultaneous goals -- nested cases;
2006-01-06 ago Pure/Isar: Toplevel.theory_to_proof admits transactions that modify the theory;
2006-01-04 ago tuned;
2006-01-04 ago * Pure/Isar: Toplevel.theory_theory_to_proof;
2006-01-03 ago Provers/classical: stricter checks to ensure that supplied intro, dest and
2006-01-03 ago rearranged burrow_split to fold_burrow to allow composition with fold_map
2006-01-03 ago * Pure/Isar: new command 'unfolding';
2005-12-31 ago * Provers/classical: removed obsolete classical version of elim_format;
2005-12-23 ago tuned;
2005-12-23 ago * Provers/induct: support simultaneous goals with mutual rules;
2005-12-23 ago is_prefix
2005-12-22 ago tuned;
2005-12-22 ago * induct: improved treatment of mutual goals and mutual rules;
2005-12-21 ago discontinued unflat in favour of burrow and burrow_split
2005-12-20 ago tuned;
2005-12-16 ago re-arranged tuples (theory * 'a) to ('a * theory) in Pure
2005-12-13 ago Provers/induct: coinduct;
2005-12-08 ago removed hint for Classical.swap, which is not really user-level anyway;
2005-12-08 ago * HOL: Theorem 'swap' is no longer bound at the ML top-level.
2005-11-30 ago simulaneous 'def';
2005-11-27 ago * Provers/induct: obtain pattern;
2005-11-25 ago tuned;
2005-11-23 ago tuned;
2005-11-23 ago Provers/induct: definitional insts and fixing;
2005-11-23 ago tuned;
2005-11-10 ago renamed Thm.cgoal_of to Thm.cprem_of;
2005-10-31 ago nth_*, fold_index refined
2005-10-28 ago tuned;
2005-10-28 ago * Pure/Isar: literal facts;
2005-10-27 ago * HOL: alternative iff syntax;
2005-10-27 ago added module Pure/General/rat.ML
2005-10-21 ago * Legacy goal package: reduced interface to the bare minimum required to keep existing proof scripts running.
2005-10-19 ago * Theory syntax: discontinued non-Isar format and old Isar headers;
2005-10-18 ago Simplifier.context/theory_context;
2005-10-17 ago * Simplifier: simpset of a running simplification process contains a proof context;
2005-10-17 ago tuned;
2005-10-15 ago tuned;
2005-10-15 ago * antiquotations ML_type, ML_struct;
2005-10-09 ago Tactics sat and satx reimplemented, several improvements
2005-10-08 ago *** empty log message ***
2005-10-07 ago tuned;
2005-10-07 ago added dummy variable binding;
2005-10-04 ago * Command 'find_theorems': support * wildcard in name: criterion.
2005-09-29 ago pdfsetup.sty: better not rely on ifpdf.sty;
2005-09-29 ago Isabelle2005 (October 2005);
2005-09-29 ago tuned;
2005-09-28 ago pointer to HOL/ex/SAT_Examples.thy added
2005-09-28 ago revert 'defs' advertisement;
2005-09-27 ago more details about incomplete 'defs';
2005-09-27 ago tuned;
2005-09-27 ago Added entries for code_module, code_library, and value.
2005-09-25 ago * Hyperreal: A theory of Taylor series.