src/HOL/HOL.thy
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 ***
1996-04-23 oheimb 1996-04-23 repaired critical proofs depending on the order inside non-confluent SimpSets, (temporarily) removed problematic rule less_Suc_eq form simpset_of "Nat"
1995-11-29 clasohm 1995-11-29 removed quotes from types in consts and syntax sections
1995-10-06 regensbu 1995-10-06 added 8bit pragmas
1995-08-18 nipkow 1995-08-18 changed "o" to (infixl 55)
1995-05-09 nipkow 1995-05-09 Prod is now a parent of Lfp. Added thm induct2 to Lfp. Changed the way patterns in abstractions are pretty printed. It has become simpler now but fails if split has more than one argument because then the ast-translation does not match.
1995-04-22 nipkow 1995-04-22 HOL.thy: "@" is no longer introduced as a "binder" but has its own explicit translation rule "@x.b" == "Eps(%x.b)". If x is a proper pattern, further translation rules for abstractions with patterns take care of the rest. This is very modular and avoids problems with "binders" such as "!" mentioned below. let now allows pttrn (let (x,y) = t in u) instead of just idt (let x = t in u) Set.thy: UN, INT, ALL, EX, etc all use "pttrn" instead of idt. Same change as for "@" above, except that "@" was a "binder" originally. Prod.thy: Added new syntax for pttrn which allows arbitrarily nested tuples. Two translation rules take care of %pttrn. Unfortunately they cannot be reversed. Hence a little ML-code is used as well. Note that now "! (x,y). ..." is syntactically valid but leads to a translation error. This is because "!" is introduced as a "binder" which means that its translation into lambda-terms is not done by a rewrite rule (aka macro) but by some fixed ML-code which comes after the rewriting stage and does not know how to handle patterns. This looks like a minor blemish since patterns in unbounded quantifiers are not that useful (well, except maybe in unique existence ...). Ideally, there should be two syntactic categories: idts, as we know and love it, which does not admit patterns. patterns, which is what idts has become now. There is one more point where patterns are now allowed but don't make sense: {e | idts . P} where idts is the list of local variables. Univ.thy: converted the defs for <++> and <**> into pattern form. It worked perfectly.
1995-03-26 nipkow 1995-03-26 Modified If_def to avoid ambiguity.
1995-03-20 clasohm 1995-03-20 changed syntax of "if"
1995-03-03 clasohm 1995-03-03 new version of HOL with curried function application