src/HOL/HOL.thy
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
2004-03-08 ballarin 2004-03-08 Added documentation for transitivity solver setup.
2004-03-04 paulson 2004-03-04 new material from Avigad, and simplified treatment of division by 0
2004-02-19 ballarin 2004-02-19 Efficient, graph-based reasoner for linear and partial orders. + Setup as solver in the HOL simplifier.
2004-01-27 paulson 2004-01-27 replacing HOL/Real/PRat, PNat by the rational number development of Markus Wenzel
2004-01-26 schirmer 2004-01-26 * Support for raw latex output in control symbols: \<^raw...> * Symbols may only start with one backslash: \<...>. \\<...> is no longer accepted by the scanner. - Adapted some Isar-theories to fit to this policy
2004-01-14 kleing 2004-01-14 print translation for ALL x <= n. P x
2003-12-15 paulson 2003-12-15 more general lemmas for Ring_and_Field
2003-10-29 berghofe 2003-10-29 Tuned proof of choice_eq.
2003-10-09 skalberg 2003-10-09 Added support for making constants final, that is, ensuring that no definition can be given later (useful for constants whose behaviour is fixed axiomatically rather than definitionally).
2003-09-26 paulson 2003-09-26 misc tidying
2003-09-23 paulson 2003-09-23 some basic new lemmas
2002-12-22 nipkow 2002-12-22 removed some problems with print translations
2002-12-22 nipkow 2002-12-22 added print translations tha avoid eta contraction for important binders.
2002-11-21 nipkow 2002-11-21 *** empty log message ***
2002-10-10 berghofe 2002-10-10 Added choice_eq.
2002-09-30 berghofe 2002-09-30 Fixed problem with induct_conj_curry: variable C should have type prop.
2002-09-30 nipkow 2002-09-30 modified induct method
2002-09-02 nipkow 2002-09-02 order_less_irrefl: [simp] -> [iff]
2002-08-30 paulson 2002-08-30 removal of blast.overloaded
2002-08-05 wenzelm 2002-08-05 special syntax for index "1" (plain numeral hidden by "1" symbol in HOL);
2002-07-31 nipkow 2002-07-31 added mk_left_commute to HOL.thy and used it "everywhere"
2002-07-24 wenzelm 2002-07-24 simplified locale predicates;
2002-07-24 wenzelm 2002-07-24 predicate defs via locales;
2002-02-25 wenzelm 2002-02-25 clarified syntax of ``long'' statements: fixes/assumes/shows;
2002-02-15 wenzelm 2002-02-15 tuned;
2002-01-06 wenzelm 2002-01-06 "_not_equal" dummy constant;
2002-01-04 wenzelm 2002-01-04 tuned ``syntax (output)'';
2001-12-10 berghofe 2001-12-10 Replaced several occurrences of "blast" by "rules".
2001-12-05 wenzelm 2001-12-05 tuned declarations (rules, sym, etc.);
2001-12-04 wenzelm 2001-12-04 setup "rules" method;
2001-12-01 wenzelm 2001-12-01 renamed class "term" to "type" (actually "HOL.type");
2001-11-24 wenzelm 2001-11-24 converted simp lemmas;
2001-11-21 wenzelm 2001-11-21 tuned;
2001-11-19 wenzelm 2001-11-19 induct method: localize rews for rule;
2001-11-12 wenzelm 2001-11-12 lemmas induct_atomize = atomize_conj ...; val local_imp_def = thm "induct_implies_def";
2001-11-09 wenzelm 2001-11-09 eliminated old "symbols" syntax, use "xsymbols" instead;
2001-11-03 wenzelm 2001-11-03 tuned;
2001-10-31 wenzelm 2001-10-31 removed obsolete (rule equal_intr_rule);
2001-10-31 wenzelm 2001-10-31 renamed inductive_XXX to induct_XXX; added induct_impliesI;
2001-10-28 wenzelm 2001-10-28 tuned declaration of rules;
2001-10-26 wenzelm 2001-10-26 atomize_conj;
2001-10-18 wenzelm 2001-10-18 setup generic cases and induction (from Inductive.thy);
2001-10-14 wenzelm 2001-10-14 moved rulify to ObjectLogic;
2001-10-14 wenzelm 2001-10-14 judgment Trueprop; proper declarations of atomize rules; incorporate theory Ord; proper section and text markup; tuned;
2001-10-12 wenzelm 2001-10-12 declare impE iffD1 iffD2 as elim of Pure;
2001-10-05 wenzelm 2001-10-05 added axclass "one" and polymorphic const "1"; print consts "0" and "1" with type constraints;
2001-10-04 wenzelm 2001-10-04 non-oriented infix = and ~= (output only); added case_split (with case names);
2001-07-25 paulson 2001-07-25 partial restructuring to reduce dependence on Axiom of Choice
2001-07-22 wenzelm 2001-07-22 declare trans [trans] (*overridden in theory Calculation*);
2001-07-20 wenzelm 2001-07-20 added "The" (definite description operator) (by Larry);