NEWS
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.
2005-09-23 ago new sat tactic
2005-09-23 ago tuned;
2005-09-23 ago ATP linkup
2005-09-23 ago *** empty log message ***
2005-09-22 ago HOLCF theorem naming conventions
2005-09-21 ago added AList.make, eq_fst, apr ...
2005-09-21 ago tunes;
2005-09-21 ago tuned;
2005-09-20 ago tuned;
2005-09-20 ago tuned;
2005-09-20 ago HOL/ex/Chinese.thy;
2005-09-20 ago infix operator precedence
2005-09-17 ago HTML.with_charset;
2005-09-17 ago Cube: converted to Isar, use locales;
2005-09-16 ago add HOLCF entries for pcpodef, cont_proc, fixrec;
2005-09-16 ago tuned
2005-09-15 ago * Improved efficiency of the Simplifier etc.;
2005-09-15 ago incorporated HOL/Hyperreal/CHANGES;
2005-09-15 ago command 'thms_containing' has been discontinued in favour of 'find_theorems';
2005-09-15 ago AList, the_*
2005-09-14 ago tuned;
2005-09-14 ago hide: added option '(open)';
2005-09-14 ago ... prem19
2005-09-14 ago Method comm_ring for proving equalities in commutative rings.
2005-09-14 ago HOL: method comm_ring;
2005-09-13 ago tuned;
2005-09-06 ago axclass: name space prefix is now "c_class" instead of just "c";