src/HOL/ex/cla.ML
1997-11-05 paulson 1997-11-05 Ran expandshort, especially to introduce Safe_tac
1997-11-03 wenzelm 1997-11-03 isatool fixclasimp;
1997-11-01 paulson 1997-11-01 mended type constraint\!
1997-10-10 wenzelm 1997-10-10 fixed dots;
1997-05-26 paulson 1997-05-26 Added a missing "result();" after problem 43.
1997-04-23 paulson 1997-04-23 Improved indentation of #34
1997-04-21 paulson 1997-04-21 Without the type constraint, the inner equality was NOT a biconditional...
1997-04-09 paulson 1997-04-09 Using Blast_tac
1997-04-04 paulson 1997-04-04 Calls Blast_tac
1997-03-04 paulson 1997-03-04 Updated reference to Pelletier erratum
1997-01-31 paulson 1997-01-31 Correction to Problem 24
1996-08-19 paulson 1996-08-19 Now starts with set_current_thy
1996-07-30 berghofe 1996-07-30 Now also Deepen_tac and Best_tac are used.
1996-06-21 berghofe 1996-06-21 Classical tactics now use default claset.
1996-05-28 paulson 1996-05-28 Corrected a comment in #34
1996-05-02 paulson 1996-05-02 Restored a proof of Pelletier #38 -- mysteriously deleted
1996-05-01 paulson 1996-05-01 Two new "obvious" examples
1996-01-30 clasohm 1996-01-30 expanded tabs
1995-12-14 paulson 1995-12-14 Added Pelletier's problem 62, as corrected in AAR Newletter #31
1995-03-22 clasohm 1995-03-22 converted ex with curried function application