src/HOL/HOL.thy
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)
1998-11-02 paulson 1998-11-02 increased precedence of unary minus from 80 to 100
1998-09-15 paulson 1998-09-15 From Compl(A) to -A
1998-08-12 oheimb 1998-08-12 cleanup for Fun.thy: merged Update.{thy|ML} into Fun.{thy|ML} moved o_def from HOL.thy to Fun.thy added Id_def to Fun.thy moved image_compose from Set.ML to Fun.ML moved o_apply and o_assoc from simpdata.ML to Fun.ML moved fun_upd_same and fun_upd_other (from Map.ML) to Fun.ML added fun_upd_twist to Fun.ML
1998-07-24 berghofe 1998-07-24 Removed ThyData setup.
1998-06-22 wenzelm 1998-06-22 isatool fixgoal;
1998-04-29 wenzelm 1998-04-29 nonterminals; tuned setup;
1998-04-04 wenzelm 1998-04-04 replaced thy_data by thy_setup;
1997-12-05 wenzelm 1997-12-05 improved arbitrary_def: we now really don't know nothing about it!
1997-11-03 wenzelm 1997-11-03 aded thy_data;
1997-10-20 wenzelm 1997-10-20 adapted to qualified names;
1997-10-10 wenzelm 1997-10-10 fixed dots;
1997-10-09 wenzelm 1997-10-09 fixed infix syntax;
1997-05-30 paulson 1997-05-30 Overloading of "^" requires new type class "power", with types "nat" and "set" in that class. The operator itself is declared in Nat.thy
1997-05-23 nipkow 1997-05-23 Added `arbitrary'
1997-05-20 wenzelm 1997-05-20 tuned;
1997-05-20 wenzelm 1997-05-20 improved output syntax of op =, op ~= (more parentheses);
1997-04-29 wenzelm 1997-04-29 deactivated new symbols (not yet printable on xterm, emacs);
1997-04-29 wenzelm 1997-04-29 added \<orelse> symbols syntax for case;
1997-04-04 nipkow 1997-04-04 moved inj and surj from Set to Fun and Inv -> inv.
1997-03-07 wenzelm 1997-03-07 fixed Not syntax;
1997-03-05 paulson 1997-03-05 Renamed constant "not" to "Not"
1997-01-24 wenzelm 1997-01-24 changed case symbol to \<Rightarrow>;
1996-12-13 oheimb 1996-12-13 adaptions for symbol font
1996-12-10 wenzelm 1996-12-10 fixed alternative quantifier symbol syntax;
1996-12-10 wenzelm 1996-12-10 fixed pris of binder syntax;
1996-11-27 wenzelm 1996-11-27 added symbols syntax;
1996-04-23 oheimb 1996-04-23 *** empty log message ***