src/HOL/HOL.thy
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);
2000-11-18 wenzelm 2000-11-18 symbol syntax for "abs";
2000-11-10 wenzelm 2000-11-10 added axclass inverse and consts inverse, divide (infix "/"); moved axclass power to Nat.thy;
2000-11-03 wenzelm 2000-11-03 "atomize" for classical tactics;
2000-09-15 paulson 2000-09-15 the final renaming: selectI -> someI
2000-09-13 wenzelm 2000-09-13 \<epsilon>: syntax (input);
2000-09-07 wenzelm 2000-09-07 removed rulify_attrib_setup;
2000-09-05 wenzelm 2000-09-05 improved meson setup;
2000-09-05 wenzelm 2000-09-05 tuned setup;
2000-09-05 paulson 2000-09-05 loads Tools/meson.ML: meson_tac installed by default
2000-08-30 nipkow 2000-08-30 Fixed rulify. As a result ?-vars in some recdef induction schemas were renamed.
2000-08-29 wenzelm 2000-08-29 cong setup now part of Simplifier;
2000-08-04 wenzelm 2000-08-04 lemmas atomize = all_eq imp_eq; setup hypsubst_setup;
2000-08-01 wenzelm 2000-08-01 added all_eq, imp_eq (for blast);
2000-07-16 wenzelm 2000-07-16 syntax (symbols) "op o" moved from HOL to Fun;
2000-06-13 wenzelm 2000-06-13 rename @case to _case_syntax (improves on low-level errors);
2000-05-24 paulson 2000-05-24 installing the plus_ac0 axclass
2000-05-23 paulson 2000-05-23 new type class "zero" so that 0 can be overloaded
2000-05-05 nipkow 2000-05-05 Added constant abs.
2000-03-31 wenzelm 2000-03-31 setup cong_attrib_setup;
2000-03-15 wenzelm 2000-03-15 splitter setup;
1999-09-01 wenzelm 1999-09-01 *: no quotes;
1999-08-26 wenzelm 1999-08-26 iff_attrib_setup;
1999-08-25 wenzelm 1999-08-25 proper bootstrap of HOL theory and packages;
1999-08-17 wenzelm 1999-08-17 replaced HOL_quantifiers flag by "HOL" print mode; simplified HOL basic syntax (more orthogonal);
1999-08-16 paulson 1999-08-16 restored a high precedence to unary minus