src/HOL/Induct/LFilter.ML
Tue, 07 Sep 1999 10:40:58 +0200 wenzelm isatool expandshort;
Tue, 19 Jan 1999 11:18:11 +0100 paulson removal of the (thm list) argument of mk_cases
Wed, 07 Oct 1998 10:31:07 +0200 paulson tidied
Fri, 31 Jul 1998 10:48:42 +0200 paulson Removal of obsolete "open" commands from heads of .ML files
Wed, 15 Jul 1998 10:15:13 +0200 paulson Removal of leading "\!\!..." from most Goal commands
Mon, 22 Jun 1998 17:26:46 +0200 wenzelm isatool fixgoal;
Sat, 07 Mar 1998 16:29:29 +0100 nipkow Removed `addsplits [expand_if]'
Thu, 08 Jan 1998 18:09:07 +0100 oheimb added select_equality to the implicit claset
Thu, 08 Jan 1998 11:21:45 +0100 paulson Tidied by adding more default simprules
Wed, 24 Dec 1997 10:02:30 +0100 paulson New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
Mon, 03 Nov 1997 12:22:43 +0100 wenzelm isatool fixclasimp;
Fri, 17 Oct 1997 15:25:12 +0200 nipkow setloop split_tac -> addsplits
Fri, 10 Oct 1997 19:02:28 +0200 wenzelm fixed dots;
Mon, 29 Sep 1997 11:37:02 +0200 paulson Step_tac -> Safe_tac
Fri, 26 Sep 1997 10:21:14 +0200 paulson Minor tidying to use Clarify_tac, etc.
Wed, 07 May 1997 12:50:26 +0200 paulson New directory to contain examples of (co)inductive definitions
less more (0) tip