src/HOL/TLA/TLA.ML
2006-07-27 wenzelm 2006-07-27 tuned proofs;
2005-09-07 wenzelm 2005-09-07 converted to Isar theory format;
2005-04-07 wenzelm 2005-04-07 reverted renaming of Some/None in comments and strings;
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2002-05-30 nipkow 2002-05-30 Modifications due to enhanced linear arithmetic.
2000-10-17 paulson 2000-10-17 renaming of contrapos rules
2000-08-03 wenzelm 2000-08-03 tuned version by Stephan Merz (unbatchified etc.);
2000-06-28 paulson 2000-06-28 fixed some abuses of addDs and addEs
1999-02-08 wenzelm 1999-02-08 updated (Stephan Merz);
1998-10-23 oheimb 1998-10-23 corrected auto_tac (applications of unsafe wrappers) improved style of several proofs
1998-09-21 oheimb 1998-09-21 improved addbefore and addSbefore improved mechanism for unsafe wrappers
1998-06-22 wenzelm 1998-06-22 isatool fixgoal;
1998-02-25 oheimb 1998-02-25 changed wrapper mechanism of classical reasoner
1997-12-24 paulson 1997-12-24 New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
1997-12-16 wenzelm 1997-12-16 expandshort;
1997-11-03 wenzelm 1997-11-03 isatool fixclasimp;
1997-10-08 wenzelm 1997-10-08 A formalization of TLA in HOL -- by Stephan Merz;