src/HOL/Lex/MaxChop.ML
Wed, 25 Oct 2000 18:39:01 +0200 wenzelm use Library/List_Prefix;
Thu, 07 Sep 2000 20:53:02 +0200 wenzelm chop_nonempty: accomodate new qed_spec_mp;
Wed, 30 Aug 2000 16:29:21 +0200 nipkow introduced induct_thm_tac
Thu, 30 Mar 2000 19:45:51 +0200 nipkow recdef.rules -> recdef.simps
Thu, 08 Jul 1999 13:44:47 +0200 paulson Now if_weak_cong is a standard congruence rule
Thu, 29 Apr 1999 18:34:30 +0200 nipkow Proof mods due to eta contraction during rewriting.
Fri, 24 Jul 1998 13:19:38 +0200 berghofe Adapted to new datatype package.
Tue, 21 Jul 1998 12:12:52 +0200 wenzelm isatool expandshort;
Sat, 18 Jul 1998 12:41:09 +0200 nipkow Simplified last proof.
Sun, 12 Jul 1998 11:49:17 +0200 wenzelm isatool expandshort;
Fri, 03 Jul 1998 10:37:04 +0200 nipkow Removed leading !! in goals.
Mon, 22 Jun 1998 17:26:46 +0200 wenzelm isatool fixgoal;
Mon, 11 May 1998 14:40:40 +0200 nipkow Reordered a few parameters.
Mon, 27 Apr 1998 16:46:56 +0200 nipkow Added conversion of reg.expr. to automata.
Tue, 10 Mar 1998 13:27:13 +0100 nipkow New scanner in abstract form.
less more (0) tip