src/HOL/HOL.thy
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
1999-08-11 nipkow 1999-08-11 * set HOL_quantifiers by default, i.e. quantifiers are printed as !/? rather than ALL/EX;
1999-07-29 paulson 1999-07-29 added parentheses to cope with a possible reduction of the precedence of unary minus
1999-06-07 wenzelm 1999-06-07 reset HOL_quantifiers by default;
1999-03-10 wenzelm 1999-03-10 HTML output;
1999-02-22 paulson 1999-02-22 added a commment on the "ext" rule
1998-12-11 oheimb 1998-12-11 added new print_mode "xsymbols" for extended symbol support (e.g. genuiely long arrows)