src/HOL/ex/MT.ML
2006-11-27 haftmann 2006-11-27 removed HOL structure
2006-10-13 berghofe 2006-10-13 Adapted to changes in FixedPoint theory.
2006-10-10 haftmann 2006-10-10 added legacy tactic
2005-10-07 nipkow 2005-10-07 changes due to new neq_simproc in simpdata.ML
2005-09-06 wenzelm 2005-09-06 converted to Isar theory format;
2004-12-08 paulson 2004-12-08 converted Lfp to new-style theory
2000-10-12 nipkow 2000-10-12 induct -> lfp_induct
2000-01-07 paulson 2000-01-07 tidied parentheses
1999-09-07 wenzelm 1999-09-07 isatool expandshort;
1998-08-06 paulson 1998-08-06 even more tidying of Goal commands
1998-07-31 paulson 1998-07-31 Removal of obsolete "open" commands from heads of .ML files
1998-07-15 paulson 1998-07-15 More tidying and removal of "\!\!... from Goal commands
1998-07-15 paulson 1998-07-15 Removal of leading "\!\!..." from most Goal commands
1998-06-22 wenzelm 1998-06-22 isatool fixgoal;
1997-12-03 paulson 1997-12-03 updated for latest Blast_tac, which treats equality differently
1997-11-05 paulson 1997-11-05 Ran expandshort, especially to introduce Safe_tac
1997-11-03 wenzelm 1997-11-03 isatool fixclasimp;
1997-10-10 wenzelm 1997-10-10 fixed dots;
1997-04-11 paulson 1997-04-11 Yet more fast_tac->blast_tac, and other tidying
1996-06-21 berghofe 1996-06-21 Classical tactics now use default claset.
1996-03-15 paulson 1996-03-15 Sets a lower value of Unify.search_bound
1996-01-30 clasohm 1996-01-30 expanded tabs
1995-10-04 clasohm 1995-10-04 added local simpsets
1995-04-13 lcp 1995-04-13 Simplified some proofs and made them work for new hyp_subst_tac.
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