src/HOL/ex/cla.ML
Thu, 12 Oct 2000 18:38:23 +0200 nipkow *** empty log message ***
Tue, 08 Jun 1999 10:25:12 +0200 paulson new classical example from Lewis Carroll via S G Pulman
Thu, 06 Aug 1998 15:48:13 +0200 paulson even more tidying of Goal commands
Thu, 16 Jul 1998 10:35:31 +0200 paulson Addition of "Theorem B" of Peter Andrews
Mon, 22 Dec 1997 12:21:37 +0100 paulson New example
Wed, 03 Dec 1997 11:00:24 +0100 paulson updated for latest Blast_tac, which treats equality differently
Wed, 05 Nov 1997 13:23:46 +0100 paulson Ran expandshort, especially to introduce Safe_tac
Mon, 03 Nov 1997 12:13:18 +0100 wenzelm isatool fixclasimp;
Sat, 01 Nov 1997 13:00:31 +0100 paulson mended type constraint\!
Fri, 10 Oct 1997 19:02:28 +0200 wenzelm fixed dots;
Mon, 26 May 1997 12:53:45 +0200 paulson Added a missing "result();" after problem 43.
Wed, 23 Apr 1997 11:05:18 +0200 paulson Improved indentation of #34
Mon, 21 Apr 1997 10:14:31 +0200 paulson Without the type constraint, the inner equality was NOT a biconditional...
Wed, 09 Apr 1997 12:32:04 +0200 paulson Using Blast_tac
Fri, 04 Apr 1997 11:18:52 +0200 paulson Calls Blast_tac
Tue, 04 Mar 1997 10:21:16 +0100 paulson Updated reference to Pelletier erratum
Fri, 31 Jan 1997 17:50:47 +0100 paulson Correction to Problem 24
Mon, 19 Aug 1996 11:19:16 +0200 paulson Now starts with set_current_thy
Tue, 30 Jul 1996 18:03:11 +0200 berghofe Now also Deepen_tac and Best_tac are used.
Fri, 21 Jun 1996 12:18:50 +0200 berghofe Classical tactics now use default claset.
Tue, 28 May 1996 11:16:38 +0200 paulson Corrected a comment in #34
Thu, 02 May 1996 12:00:37 +0200 paulson Restored a proof of Pelletier #38 -- mysteriously deleted
Wed, 01 May 1996 13:47:21 +0200 paulson Two new "obvious" examples
Tue, 30 Jan 1996 15:24:36 +0100 clasohm expanded tabs
Thu, 14 Dec 1995 12:49:32 +0100 paulson Added Pelletier's problem 62, as corrected in AAR
Wed, 22 Mar 1995 12:42:34 +0100 clasohm converted ex with curried function application
less more (0) tip