src/HOL/HOL.thy
1998-07-24 berghofe Removed ThyData setup.
1998-06-22 wenzelm isatool fixgoal;
1998-04-29 wenzelm nonterminals;
1998-04-04 wenzelm replaced thy_data by thy_setup;
1997-12-05 wenzelm improved arbitrary_def: we now really don't know nothing about it!
1997-11-03 wenzelm aded thy_data;
1997-10-20 wenzelm adapted to qualified names;
1997-10-10 wenzelm fixed dots;
1997-10-09 wenzelm fixed infix syntax;
1997-05-30 paulson Overloading of "^" requires new type class "power", with types "nat" and
1997-05-23 nipkow Added `arbitrary'
1997-05-20 wenzelm tuned;
1997-05-20 wenzelm improved output syntax of op =, op ~= (more parentheses);
1997-04-29 wenzelm deactivated new symbols (not yet printable on xterm, emacs);
1997-04-29 wenzelm added \<orelse> symbols syntax for case;
1997-04-04 nipkow moved inj and surj from Set to Fun and Inv -> inv.
1997-03-07 wenzelm fixed Not syntax;
1997-03-05 paulson Renamed constant "not" to "Not"
1997-01-24 wenzelm changed case symbol to \<Rightarrow>;
1996-12-13 oheimb adaptions for symbol font
1996-12-10 wenzelm fixed alternative quantifier symbol syntax;
1996-12-10 wenzelm fixed pris of binder syntax;
1996-11-27 wenzelm added symbols syntax;
1996-04-23 oheimb *** empty log message ***
1996-04-23 oheimb repaired critical proofs depending on the order inside non-confluent SimpSets,
1995-11-29 clasohm removed quotes from types in consts and syntax sections
1995-10-06 regensbu added 8bit pragmas
1995-08-18 nipkow changed "o" to (infixl 55)
1995-05-09 nipkow Prod is now a parent of Lfp.
1995-04-22 nipkow HOL.thy:
1995-03-26 nipkow Modified If_def to avoid ambiguity.
1995-03-20 clasohm changed syntax of "if"
1995-03-03 clasohm new version of HOL with curried function application
less more (0) tip