src/HOL/HOL.thy
2006-01-19 ago setup: theory -> theory;
2006-01-17 ago substantial improvements in code generator
2006-01-16 ago declare the1_equality [elim?];
2006-01-15 ago prefer ex1I over ex_ex1I in single-step reasoning;
2006-01-06 ago simplified EqSubst setup;
2006-01-06 ago tuned EqSubst setup;
2005-12-31 ago removed obsolete cla_dist_concl;
2005-12-30 ago provide cla_dist_concl;
2005-12-23 ago removed obsolete induct_atomize_old;
2005-12-22 ago structure ProjectRule;
2005-10-27 ago alternative iff syntax for equality on booleans, with print_mode 'iff';
2005-09-25 ago eq_codegen now ensures that code for bool type is generated.
2005-09-22 ago renamed rules to iprover
2005-09-17 ago added code generator setup (from Main.thy);
2005-09-15 ago the experimental tagging system, and the usual tidying
2005-09-06 ago axclass: name space prefix is now "c_class" instead of just "c";
2005-08-31 ago simp_implies: proper named infix;
2005-08-02 ago Turned simp_implies into binary operator.
2005-07-12 ago added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
2005-07-01 ago Implemented trick (due to Tobias Nipkow) for fine-tuning simplification
2005-06-28 ago Constant "If" is now local
2005-06-17 ago migrated theory headers to new format
2005-05-31 ago tuned;
2005-05-22 ago Simplifier already setup in Pure;
2005-04-21 ago superceded by Pure.thy and CPure.thy;
2005-04-07 ago new meta-level rules
2005-04-05 ago arg_cong2 by Norbert Voelker
2005-03-03 ago Move towards standard functions.
2005-02-10 ago Moved oderings from HOL into the new Orderings.thy
2005-02-01 ago the new subst tactic, by Lucas Dixon
2004-12-18 ago added simproc for Let
2004-12-15 ago removal of HOL_Lemmas
2004-12-07 ago proof of subst by S Merz
2004-12-02 ago Fixed print translation for ALL x > y etc
2004-12-02 ago added ALL print-translation for > and >=.
2004-12-02 ago Added "ALL x > y" and relatives.
2004-12-01 ago Added > and >= sugar
2004-11-15 ago removed a "clone" (duplicate code)
2004-09-10 ago Added antisymmetry simproc
2004-08-18 ago import -> imports
2004-08-16 ago New theory header syntax.
2004-08-03 ago New transitivity reasoners for transitivity only and quasi orders.
2004-07-28 ago conversion of Hyperreal/MacLaurin_lemmas to Isar script
2004-06-21 ago Merged in license change from Isabelle2004
2004-06-01 ago removed obsolete sort 'logic';
2004-05-14 ago new atomize theorem
2004-05-01 ago _index1: accomodate improved indexed syntax;
2004-04-16 ago simplified ML code for setsubgoaler;
2004-04-14 ago use more symbols in HTML output
2004-03-08 ago Added documentation for transitivity solver setup.
2004-03-04 ago new material from Avigad, and simplified treatment of division by 0
2004-02-19 ago Efficient, graph-based reasoner for linear and partial orders.
2004-01-27 ago replacing HOL/Real/PRat, PNat by the rational number development
2004-01-26 ago * Support for raw latex output in control symbols: \<^raw...>
2004-01-14 ago print translation for ALL x <= n. P x
2003-12-15 ago more general lemmas for Ring_and_Field
2003-10-29 ago Tuned proof of choice_eq.
2003-10-09 ago Added support for making constants final, that is, ensuring that no
2003-09-26 ago misc tidying
2003-09-23 ago some basic new lemmas