src/Provers/simplifier.ML
Mon, 14 Feb 2000 20:43:12 +0100 wenzelm easy_setup: fixed mksimps;
Thu, 10 Feb 2000 13:34:52 +0100 wenzelm added easy_setup;
Sat, 29 Jan 2000 14:22:16 +0100 wenzelm simp_all method;
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, 29 Sep 1999 14:36:04 +0200 wenzelm mk_simps: do *not* include Thm.strip_shyps o Drule.zero_var_indexes
Tue, 21 Sep 1999 23:06:50 +0200 wenzelm merged in lost update;
Tue, 21 Sep 1999 19:05:38 +0200 nipkow Solvers are now named and stamped.
Tue, 21 Sep 1999 17:26:42 +0200 wenzelm setup for refined facts handling;
Wed, 01 Sep 1999 21:22:38 +0200 wenzelm Method.insert_tac;
Wed, 18 Aug 1999 20:48:06 +0200 wenzelm Method.modifier;
Mon, 16 Aug 1999 17:44:14 +0200 oheimb forgot to write back adaption of onlysimps
Mon, 16 Aug 1999 17:33:45 +0200 oheimb exchanged finish_tac and unsafe_finish_tac (the more important one) in simpset
Thu, 05 Aug 1999 22:09:23 +0200 wenzelm change_simpset_of;
Fri, 30 Jul 1999 13:43:26 +0200 wenzelm eliminated METHOD0 in favour of same_tac;
Tue, 13 Jul 1999 12:32:22 +0200 wenzelm same_tac;
Tue, 06 Jul 1999 21:16:29 +0200 wenzelm simp only: attribute, method arg;
Fri, 30 Apr 1999 18:10:03 +0200 wenzelm theory data: copy;
Tue, 27 Apr 1999 15:39:43 +0200 wenzelm improper simp methods;
Wed, 17 Mar 1999 16:33:47 +0100 wenzelm Theory.sign_of;
Tue, 12 Jan 1999 15:25:53 +0100 wenzelm eliminated tthm type and Attribute structure;
Wed, 18 Nov 1998 11:02:42 +0100 wenzelm export simp_modifiers;
Mon, 16 Nov 1998 11:10:00 +0100 wenzelm all modifiers turned into attributes;
Mon, 09 Nov 1998 15:50:56 +0100 wenzelm local simpset theory data;
Thu, 25 Jun 1998 15:33:30 +0200 wenzelm added XX_YY_rewrite: simpset -> cterm -> thm;
Wed, 10 Jun 1998 18:07:07 +0200 wenzelm Context.the_context;
Wed, 10 Jun 1998 12:00:51 +0200 wenzelm adapted to TheoryDataFun interface;
Fri, 05 Jun 1998 14:33:18 +0200 wenzelm accomodate tuned version of theory data;
Wed, 29 Apr 1998 11:30:55 +0200 wenzelm tuned setup;
Sat, 04 Apr 1998 12:30:17 +0200 wenzelm tuned comments;
Fri, 03 Apr 1998 14:38:19 +0200 wenzelm tuned names;
Thu, 12 Mar 1998 13:13:19 +0100 oheimb addloop: added warning in case of overwriting a looper
Thu, 12 Mar 1998 12:48:49 +0100 nipkow Used merge_alists for loopers.
Tue, 10 Mar 1998 19:02:20 +0100 nipkow The new asm_lr_simp_tac is the old asm_full_simp_tac.
Tue, 10 Mar 1998 13:24:11 +0100 nipkow New simplifier flag for mutual simplification.
Fri, 06 Mar 1998 15:20:29 +0100 nipkow Added delspilts, Addsplits, Delsplits.
Wed, 04 Mar 1998 13:14:11 +0100 nipkow Reorganized simplifier. May now reorient rules.
Sat, 28 Feb 1998 15:40:50 +0100 nipkow Little reorganization. Loop tactics have names now.
Mon, 09 Feb 1998 14:40:59 +0100 nipkow Used THEN_ALL_NEW.
Thu, 04 Dec 1997 14:11:37 +0100 wenzelm added print_simpset;
Wed, 26 Nov 1997 16:41:51 +0100 wenzelm removed conv_prover;
Fri, 21 Nov 1997 15:29:56 +0100 wenzelm changed Pure/Sequence interface -- isatool fixseq;
Thu, 20 Nov 1997 15:36:09 +0100 wenzelm adapted print methods;
Tue, 04 Nov 1997 16:17:04 +0100 wenzelm type object = exn (enhance readability);
Mon, 03 Nov 1997 11:56:53 +0100 wenzelm new implicit simpset mechanism based on Sign.sg anytype data;
Mon, 29 Sep 1997 11:45:52 +0200 paulson Default simpset tactics now dereference "simpset"
Fri, 25 Jul 1997 13:18:09 +0200 wenzelm added prems argument to simplification procedures;
Wed, 23 Jul 1997 11:03:54 +0200 wenzelm added simplification meta rules;
Tue, 22 Jul 1997 18:46:44 +0200 wenzelm added print_ss;
Tue, 22 Jul 1997 11:12:55 +0200 paulson Removal of the tactical STATE
Wed, 16 Jul 1997 11:34:42 +0200 wenzelm fixed merge of internal simprocs;
Mon, 17 Feb 1997 13:54:24 +0100 wenzelm mk_rews: automatically includes strip_shyps, zero_var_indexes;
Sat, 15 Feb 1997 16:14:35 +0100 oheimb added deleqcongs, richer rep_ss
Fri, 31 Jan 1997 15:54:00 +0100 oheimb added addloop (and also documentation of addsolver
Fri, 17 Jan 1997 18:19:57 +0100 wenzelm addsimps, addeqcongs: replaced @ by gen_union;
Thu, 16 Jan 1997 14:53:37 +0100 wenzelm added termless parameter;
Fri, 10 Jan 1997 10:27:57 +0100 wenzelm cleaned up (real changes next time);
Wed, 29 May 1996 12:03:32 +0200 nipkow Added addsolver
Tue, 23 Apr 1996 17:11:23 +0200 oheimb *** empty log message ***
Fri, 16 Feb 1996 18:00:47 +0100 paulson Elimination of fully-functorial style.
less more (0) -60 tip