src/HOL/HOL.thy
2006-04-06 haftmann 2006-04-06 adapted for definitional code generation
2006-03-10 haftmann 2006-03-10 renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
2006-03-02 paulson 2006-03-02 moved the "use" directive
2006-03-01 mengj 2006-03-01 Added setup for "atpset" (a rule set for ATPs).
2006-02-25 haftmann 2006-02-25 improved codegen bootstrap
2006-02-22 wenzelm 2006-02-22 simplified Pure conjunction;
2006-02-14 haftmann 2006-02-14 added theory of executable rational numbers
2006-02-01 berghofe 2006-02-01 Added "evaluation" method and oracle.
2006-01-31 haftmann 2006-01-31 added serialization for arbitrary
2006-01-29 wenzelm 2006-01-29 declare 'defn' rules;
2006-01-23 haftmann 2006-01-23 removed problematic keyword 'atom'
2006-01-19 wenzelm 2006-01-19 setup: theory -> theory;
2006-01-17 haftmann 2006-01-17 substantial improvements in code generator
2006-01-16 wenzelm 2006-01-16 declare the1_equality [elim?];
2006-01-15 wenzelm 2006-01-15 prefer ex1I over ex_ex1I in single-step reasoning;
2006-01-06 wenzelm 2006-01-06 simplified EqSubst setup;
2006-01-06 wenzelm 2006-01-06 tuned EqSubst setup;
2005-12-31 wenzelm 2005-12-31 removed obsolete cla_dist_concl;
2005-12-30 wenzelm 2005-12-30 provide cla_dist_concl;
2005-12-23 wenzelm 2005-12-23 removed obsolete induct_atomize_old;
2005-12-22 wenzelm 2005-12-22 structure ProjectRule; updated auxiliary facts for induct method; tuned proofs;
2005-10-27 wenzelm 2005-10-27 alternative iff syntax for equality on booleans, with print_mode 'iff';
2005-09-25 berghofe 2005-09-25 eq_codegen now ensures that code for bool type is generated.
2005-09-22 nipkow 2005-09-22 renamed rules to iprover
2005-09-17 wenzelm 2005-09-17 added code generator setup (from Main.thy);
2005-09-15 paulson 2005-09-15 the experimental tagging system, and the usual tidying
2005-09-06 wenzelm 2005-09-06 axclass: name space prefix is now "c_class" instead of just "c";
2005-08-31 wenzelm 2005-08-31 simp_implies: proper named infix;
2005-08-02 ballarin 2005-08-02 Turned simp_implies into binary operator.
2005-07-12 avigad 2005-07-12 added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities) added lemmas to Ring_and_Field.thy (reasoning about signs, fractions, etc.) renamed simplification rules for abs (abs_of_pos, etc.) renamed rules for multiplication and signs (mult_pos_pos, etc.) moved lemmas involving fractions from NatSimprocs.thy added setsum_mono3 to FiniteSet.thy added simplification rules for powers to Parity.thy
2005-07-01 berghofe 2005-07-01 Implemented trick (due to Tobias Nipkow) for fine-tuning simplification of premises of congruence rules.
2005-06-28 paulson 2005-06-28 Constant "If" is now local
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2005-05-31 wenzelm 2005-05-31 tuned;
2005-05-22 wenzelm 2005-05-22 Simplifier already setup in Pure;
2005-04-21 wenzelm 2005-04-21 superceded by Pure.thy and CPure.thy;
2005-04-07 paulson 2005-04-07 new meta-level rules
2005-04-05 paulson 2005-04-05 arg_cong2 by Norbert Voelker
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-10 nipkow 2005-02-10 Moved oderings from HOL into the new Orderings.thy
2005-02-01 paulson 2005-02-01 the new subst tactic, by Lucas Dixon
2004-12-18 schirmer 2004-12-18 added simproc for Let
2004-12-15 paulson 2004-12-15 removal of HOL_Lemmas
2004-12-07 paulson 2004-12-07 proof of subst by S Merz
2004-12-02 nipkow 2004-12-02 Fixed print translation for ALL x > y etc
2004-12-02 nipkow 2004-12-02 added ALL print-translation for > and >=.
2004-12-02 nipkow 2004-12-02 Added "ALL x > y" and relatives.
2004-12-01 nipkow 2004-12-01 Added > and >= sugar
2004-11-15 paulson 2004-11-15 removed a "clone" (duplicate code)
2004-09-10 nipkow 2004-09-10 Added antisymmetry simproc
2004-08-18 nipkow 2004-08-18 import -> imports
2004-08-16 nipkow 2004-08-16 New theory header syntax.
2004-08-03 ballarin 2004-08-03 New transitivity reasoners for transitivity only and quasi orders.
2004-07-28 paulson 2004-07-28 conversion of Hyperreal/MacLaurin_lemmas to Isar script
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2004-06-01 wenzelm 2004-06-01 removed obsolete sort 'logic';
2004-05-14 paulson 2004-05-14 new atomize theorem
2004-05-01 wenzelm 2004-05-01 _index1: accomodate improved indexed syntax;
2004-04-16 wenzelm 2004-04-16 simplified ML code for setsubgoaler;
2004-04-14 kleing 2004-04-14 use more symbols in HTML output