src/Provers/clasimp.ML
Wed, 20 Sep 2000 00:02:26 +0200 wenzelm made SML/NJ happy;
Tue, 19 Sep 2000 23:52:37 +0200 wenzelm added iff_add_global', iff_add_local' (syntax "iff?");
Wed, 13 Sep 2000 22:31:19 +0200 wenzelm Args.addN, Args.delN;
Thu, 07 Sep 2000 20:51:07 +0200 wenzelm tuned msg;
Tue, 05 Sep 2000 18:50:12 +0200 wenzelm added 'iff' declarations;
Sat, 02 Sep 2000 21:51:14 +0200 wenzelm added "slowsimp", "bestsimp";
Fri, 01 Sep 2000 00:31:08 +0200 wenzelm auto method: opt args;
Mon, 14 Aug 2000 14:53:26 +0200 wenzelm added "fastsimp";
Thu, 03 Aug 2000 00:44:49 +0200 wenzelm export get_local_clasimpset, clasimp_modifiers;
Tue, 25 Jul 2000 00:13:11 +0200 wenzelm added clarsimp method;
Fri, 21 Jul 2000 17:46:43 +0200 oheimb strengthened force_tac by using new first_best_tac
Fri, 31 Mar 2000 21:58:34 +0200 wenzelm added change_global/local_css;
Wed, 15 Mar 2000 18:40:03 +0100 wenzelm include Splitter.split_modifiers;
Fri, 28 Jan 2000 21:57:15 +0100 wenzelm HEADGOAL;
Fri, 28 Jan 2000 12:12:06 +0100 wenzelm replaced FIRSTGOAL by FINDGOAL (backtracking!);
Wed, 27 Oct 1999 19:29:47 +0200 oheimb clarsimp_tac now copes with the (unwanted) case that the simplifier splits
Tue, 21 Sep 1999 17:26:50 +0200 wenzelm setup for refined facts handling;
Thu, 02 Sep 1999 15:21:36 +0200 wenzelm renamed improper method 'clarsimp' to 'clarsimp_tac';
Wed, 01 Sep 1999 21:22:56 +0200 wenzelm Method.insert_tac;
Mon, 30 Aug 1999 17:26:43 +0200 wenzelm auto: CHANGED;
Wed, 18 Aug 1999 20:47:31 +0200 wenzelm Method.modifier;
Mon, 02 Aug 1999 17:58:46 +0200 wenzelm tuned;
Fri, 30 Jul 1999 13:43:26 +0200 wenzelm eliminated METHOD0 in favour of same_tac;
Sun, 29 Nov 1998 13:13:57 +0100 wenzelm method brute_force = ALLGOALS force_tac;
Wed, 18 Nov 1998 11:01:48 +0100 wenzelm method setup;
Fri, 23 Oct 1998 20:35:56 +0200 oheimb corrected auto_tac (applications of unsafe wrappers)
Fri, 25 Sep 1998 14:06:00 +0200 paulson deleted illegal "op"
Thu, 24 Sep 1998 17:17:56 +0200 oheimb removed addcongs2 and delcongs2
Mon, 21 Sep 1998 23:17:28 +0200 oheimb improved addbefore and addSbefore
Fri, 11 Sep 1998 17:20:58 +0200 oheimb added clarsimp_tac and Clarsimp_tac
Thu, 30 Jul 1998 19:02:52 +0200 wenzelm functorized Clasimp module;
Sat, 02 May 1998 16:46:17 +0200 wenzelm added CLASIMPSET(') tacticals;
Fri, 01 May 1998 22:30:42 +0200 oheimb Auto_tac: now uses enhanced version of asm_full_simp_tac,
Tue, 10 Mar 1998 18:26:27 +0100 oheimb renamed smart_tac to force_tac, slight improvement of force_tac
Thu, 26 Feb 1998 15:45:33 +0100 oheimb added smart_tac
Wed, 25 Feb 1998 20:25:27 +0100 oheimb factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
less more (0) tip