src/HOL/ex/MT.thy
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2013-02-28 wenzelm 2013-02-28 eliminated legacy 'axioms';
2011-05-13 wenzelm 2011-05-13 proper Proof.context for classical tactics; reduced claset to snapshot of classical context; discontinued clasimpset;
2011-01-07 bulwahn 2011-01-07 removing obselete Id comments from HOL/ex theories
2007-08-18 wenzelm 2007-08-18 converted ex/MT.ML;
2005-09-06 wenzelm 2005-09-06 converted to Isar theory format;
2005-01-21 paulson 2005-01-21 inserted quotes preparatory to conversion
2001-12-01 wenzelm 2001-12-01 renamed class "term" to "type" (actually "HOL.type");
1998-06-30 berghofe 1998-06-30 Adapted to new inductive definition package.
1997-10-10 wenzelm 1997-10-10 fixed dots;
1996-02-05 clasohm 1996-02-05 expanded tabs; incorporated Konrad's changes
1995-12-01 clasohm 1995-12-01 removed quotes from consts and syntax sections
1995-06-21 clasohm 1995-06-21 removed \...\ inside strings
1995-04-10 nipkow 1995-04-10 ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them. MT.thy: Deleted extra space in clos_mk.
1995-03-24 clasohm 1995-03-24 changed syntax of tuples from <..., ...> to (..., ...)
1995-03-22 clasohm 1995-03-22 converted ex with curried function application