| Fri, 15 Apr 2005 12:00:00 +0200 |
ballarin |
Removed most of the atp interface from Pure.
|
file |
diff |
annotate
|
| Sun, 13 Feb 2005 17:15:14 +0100 |
skalberg |
Deleted Library.option type.
|
file |
diff |
annotate
|
| Thu, 03 Feb 2005 16:45:59 +0100 |
nipkow |
added find_rewrites
|
file |
diff |
annotate
|
| Fri, 21 Jan 2005 18:00:18 +0100 |
paulson |
Jia Meng: delta simpsets and clasets
|
file |
diff |
annotate
|
| Sun, 11 Jul 2004 20:35:50 +0200 |
wenzelm |
context dependent components;
|
file |
diff |
annotate
|
| Thu, 08 Jul 2004 19:34:00 +0200 |
wenzelm |
got rid of obsolete meta_simpset; tuned;
|
file |
diff |
annotate
|
| Fri, 25 Jun 2004 14:30:55 +0200 |
skalberg |
Merging the meta-simplifier with the Provers-simplifier. Next step:
|
file |
diff |
annotate
|
| Fri, 28 May 2004 21:09:56 +0200 |
schirmer |
added asm_lr_simplify/asm_lr_rewrite and adapted asm_full_simplify/asm_full_rewrite to match to corresponding simp_tacs
|
file |
diff |
annotate
|
| Mon, 30 Sep 2002 16:36:57 +0200 |
berghofe |
Added syntax for "asm_lr" simplifier option.
|
file |
diff |
annotate
|
| Wed, 07 Aug 2002 20:03:38 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 06 Aug 2002 11:22:05 +0200 |
wenzelm |
sane interface for simprocs;
|
file |
diff |
annotate
|
| Wed, 28 Nov 2001 00:46:26 +0100 |
wenzelm |
theory data: removed obsolete finish method;
|
file |
diff |
annotate
|
| Sat, 24 Nov 2001 16:54:32 +0100 |
wenzelm |
generic_merge;
|
file |
diff |
annotate
|
| Thu, 08 Nov 2001 23:59:37 +0100 |
wenzelm |
theory data: finish method;
|
file |
diff |
annotate
|
| Thu, 25 Oct 2001 22:42:50 +0200 |
wenzelm |
'simplified' att: args;
|
file |
diff |
annotate
|
| Thu, 04 Oct 2001 15:19:56 +0200 |
wenzelm |
qualify MetaSimplifier;
|
file |
diff |
annotate
|
| Sun, 07 Jan 2001 21:41:56 +0100 |
wenzelm |
CHANGED_PROP;
|
file |
diff |
annotate
|
| Tue, 07 Nov 2000 17:42:19 +0100 |
berghofe |
Moved meta simplification stuff from Thm to MetaSimplifier.
|
file |
diff |
annotate
|
| Tue, 19 Sep 2000 23:53:00 +0200 |
wenzelm |
tuned args;
|
file |
diff |
annotate
|
| Fri, 15 Sep 2000 21:52:09 +0200 |
wenzelm |
safe_asm_full_simp_tac is back (for compat);
|
file |
diff |
annotate
|
| Wed, 13 Sep 2000 22:31:19 +0200 |
wenzelm |
Args.addN, Args.delN;
|
file |
diff |
annotate
|
| Thu, 07 Sep 2000 20:56:04 +0200 |
wenzelm |
tuned att names / msgs;
|
file |
diff |
annotate
|
| Tue, 05 Sep 2000 18:50:30 +0200 |
wenzelm |
removed 'other' modifier;
|
file |
diff |
annotate
|
| Tue, 29 Aug 2000 12:28:48 +0200 |
wenzelm |
made SML/XL happy;
|
file |
diff |
annotate
|
| Tue, 29 Aug 2000 00:56:22 +0200 |
wenzelm |
proper cong setup;
|
file |
diff |
annotate
|
| Thu, 03 Aug 2000 18:44:24 +0200 |
wenzelm |
unknown_theory/proof/context;
|
file |
diff |
annotate
|
| Tue, 25 Jul 2000 23:33:13 +0200 |
wenzelm |
tuned msg;
|
file |
diff |
annotate
|
| Fri, 21 Jul 2000 17:46:38 +0200 |
oheimb |
removed safe_asm_full_simp_tac
|
file |
diff |
annotate
|
| Wed, 31 May 2000 14:29:42 +0200 |
wenzelm |
Toplevel.no_timing;
|
file |
diff |
annotate
|
| Wed, 17 May 2000 17:16:21 +0200 |
wenzelm |
export generic_simp_tac;
|
file |
diff |
annotate
|
| Fri, 05 May 2000 22:32:25 +0200 |
wenzelm |
use Args.colon / Args.parens;
|
file |
diff |
annotate
|
| Mon, 17 Apr 2000 14:10:04 +0200 |
wenzelm |
Pretty.chunks;
|
file |
diff |
annotate
|
| Thu, 13 Apr 2000 15:01:11 +0200 |
wenzelm |
added simp_options;
|
file |
diff |
annotate
|
| Tue, 04 Apr 2000 22:16:11 +0200 |
wenzelm |
print_simpset / print_claset command;
|
file |
diff |
annotate
|
| Fri, 31 Mar 2000 21:55:27 +0200 |
wenzelm |
use Attrib.add_del_args;
|
file |
diff |
annotate
|
| Wed, 15 Mar 2000 18:36:53 +0100 |
wenzelm |
export change_global_ss, change_local_ss;
|
file |
diff |
annotate
|
| Wed, 08 Mar 2000 23:47:44 +0100 |
wenzelm |
fixed section syntax;
|
file |
diff |
annotate
|
| Mon, 14 Feb 2000 20:43:12 +0100 |
wenzelm |
easy_setup: fixed mksimps;
|
file |
diff |
annotate
|
| Thu, 10 Feb 2000 13:34:52 +0100 |
wenzelm |
added easy_setup;
|
file |
diff |
annotate
|
| Sat, 29 Jan 2000 14:22:16 +0100 |
wenzelm |
simp_all method;
|
file |
diff |
annotate
|
| Fri, 28 Jan 2000 21:57:15 +0100 |
wenzelm |
HEADGOAL;
|
file |
diff |
annotate
|
| Fri, 28 Jan 2000 12:12:06 +0100 |
wenzelm |
replaced FIRSTGOAL by FINDGOAL (backtracking!);
|
file |
diff |
annotate
|
| Wed, 29 Sep 1999 14:36:04 +0200 |
wenzelm |
mk_simps: do *not* include Thm.strip_shyps o Drule.zero_var_indexes
|
file |
diff |
annotate
|
| Tue, 21 Sep 1999 23:06:50 +0200 |
wenzelm |
merged in lost update;
|
file |
diff |
annotate
|
| Tue, 21 Sep 1999 19:05:38 +0200 |
nipkow |
Solvers are now named and stamped.
|
file |
diff |
annotate
|
| Tue, 21 Sep 1999 17:26:42 +0200 |
wenzelm |
setup for refined facts handling;
|
file |
diff |
annotate
|
| Wed, 01 Sep 1999 21:22:38 +0200 |
wenzelm |
Method.insert_tac;
|
file |
diff |
annotate
|
| Wed, 18 Aug 1999 20:48:06 +0200 |
wenzelm |
Method.modifier;
|
file |
diff |
annotate
|
| Mon, 16 Aug 1999 17:44:14 +0200 |
oheimb |
forgot to write back adaption of onlysimps
|
file |
diff |
annotate
|
| Mon, 16 Aug 1999 17:33:45 +0200 |
oheimb |
exchanged finish_tac and unsafe_finish_tac (the more important one) in simpset
|
file |
diff |
annotate
|
| Thu, 05 Aug 1999 22:09:23 +0200 |
wenzelm |
change_simpset_of;
|
file |
diff |
annotate
|
| Fri, 30 Jul 1999 13:43:26 +0200 |
wenzelm |
eliminated METHOD0 in favour of same_tac;
|
file |
diff |
annotate
|
| Tue, 13 Jul 1999 12:32:22 +0200 |
wenzelm |
same_tac;
|
file |
diff |
annotate
|
| Tue, 06 Jul 1999 21:16:29 +0200 |
wenzelm |
simp only: attribute, method arg;
|
file |
diff |
annotate
|
| Fri, 30 Apr 1999 18:10:03 +0200 |
wenzelm |
theory data: copy;
|
file |
diff |
annotate
|
| Tue, 27 Apr 1999 15:39:43 +0200 |
wenzelm |
improper simp methods;
|
file |
diff |
annotate
|
| Wed, 17 Mar 1999 16:33:47 +0100 |
wenzelm |
Theory.sign_of;
|
file |
diff |
annotate
|
| Tue, 12 Jan 1999 15:25:53 +0100 |
wenzelm |
eliminated tthm type and Attribute structure;
|
file |
diff |
annotate
|
| Wed, 18 Nov 1998 11:02:42 +0100 |
wenzelm |
export simp_modifiers;
|
file |
diff |
annotate
|
| Mon, 16 Nov 1998 11:10:00 +0100 |
wenzelm |
all modifiers turned into attributes;
|
file |
diff |
annotate
|
| Mon, 09 Nov 1998 15:50:56 +0100 |
wenzelm |
local simpset theory data;
|
file |
diff |
annotate
|
| Thu, 25 Jun 1998 15:33:30 +0200 |
wenzelm |
added XX_YY_rewrite: simpset -> cterm -> thm;
|
file |
diff |
annotate
|
| Wed, 10 Jun 1998 18:07:07 +0200 |
wenzelm |
Context.the_context;
|
file |
diff |
annotate
|
| Wed, 10 Jun 1998 12:00:51 +0200 |
wenzelm |
adapted to TheoryDataFun interface;
|
file |
diff |
annotate
|
| Fri, 05 Jun 1998 14:33:18 +0200 |
wenzelm |
accomodate tuned version of theory data;
|
file |
diff |
annotate
|
| Wed, 29 Apr 1998 11:30:55 +0200 |
wenzelm |
tuned setup;
|
file |
diff |
annotate
|
| Sat, 04 Apr 1998 12:30:17 +0200 |
wenzelm |
tuned comments;
|
file |
diff |
annotate
|
| Fri, 03 Apr 1998 14:38:19 +0200 |
wenzelm |
tuned names;
|
file |
diff |
annotate
|
| Thu, 12 Mar 1998 13:13:19 +0100 |
oheimb |
addloop: added warning in case of overwriting a looper
|
file |
diff |
annotate
|
| Thu, 12 Mar 1998 12:48:49 +0100 |
nipkow |
Used merge_alists for loopers.
|
file |
diff |
annotate
|
| Tue, 10 Mar 1998 19:02:20 +0100 |
nipkow |
The new asm_lr_simp_tac is the old asm_full_simp_tac.
|
file |
diff |
annotate
|
| Tue, 10 Mar 1998 13:24:11 +0100 |
nipkow |
New simplifier flag for mutual simplification.
|
file |
diff |
annotate
|
| Fri, 06 Mar 1998 15:20:29 +0100 |
nipkow |
Added delspilts, Addsplits, Delsplits.
|
file |
diff |
annotate
|
| Wed, 04 Mar 1998 13:14:11 +0100 |
nipkow |
Reorganized simplifier. May now reorient rules.
|
file |
diff |
annotate
|
| Sat, 28 Feb 1998 15:40:50 +0100 |
nipkow |
Little reorganization. Loop tactics have names now.
|
file |
diff |
annotate
|
| Mon, 09 Feb 1998 14:40:59 +0100 |
nipkow |
Used THEN_ALL_NEW.
|
file |
diff |
annotate
|
| Thu, 04 Dec 1997 14:11:37 +0100 |
wenzelm |
added print_simpset;
|
file |
diff |
annotate
|
| Wed, 26 Nov 1997 16:41:51 +0100 |
wenzelm |
removed conv_prover;
|
file |
diff |
annotate
|
| Fri, 21 Nov 1997 15:29:56 +0100 |
wenzelm |
changed Pure/Sequence interface -- isatool fixseq;
|
file |
diff |
annotate
|
| Thu, 20 Nov 1997 15:36:09 +0100 |
wenzelm |
adapted print methods;
|
file |
diff |
annotate
|
| Tue, 04 Nov 1997 16:17:04 +0100 |
wenzelm |
type object = exn (enhance readability);
|
file |
diff |
annotate
|
| Mon, 03 Nov 1997 11:56:53 +0100 |
wenzelm |
new implicit simpset mechanism based on Sign.sg anytype data;
|
file |
diff |
annotate
|
| Mon, 29 Sep 1997 11:45:52 +0200 |
paulson |
Default simpset tactics now dereference "simpset"
|
file |
diff |
annotate
|
| Fri, 25 Jul 1997 13:18:09 +0200 |
wenzelm |
added prems argument to simplification procedures;
|
file |
diff |
annotate
|
| Wed, 23 Jul 1997 11:03:54 +0200 |
wenzelm |
added simplification meta rules;
|
file |
diff |
annotate
|
| Tue, 22 Jul 1997 18:46:44 +0200 |
wenzelm |
added print_ss;
|
file |
diff |
annotate
|
| Tue, 22 Jul 1997 11:12:55 +0200 |
paulson |
Removal of the tactical STATE
|
file |
diff |
annotate
|
| Wed, 16 Jul 1997 11:34:42 +0200 |
wenzelm |
fixed merge of internal simprocs;
|
file |
diff |
annotate
|
| Mon, 17 Feb 1997 13:54:24 +0100 |
wenzelm |
mk_rews: automatically includes strip_shyps, zero_var_indexes;
|
file |
diff |
annotate
|
| Sat, 15 Feb 1997 16:14:35 +0100 |
oheimb |
added deleqcongs, richer rep_ss
|
file |
diff |
annotate
|
| Fri, 31 Jan 1997 15:54:00 +0100 |
oheimb |
added addloop (and also documentation of addsolver
|
file |
diff |
annotate
|
| Fri, 17 Jan 1997 18:19:57 +0100 |
wenzelm |
addsimps, addeqcongs: replaced @ by gen_union;
|
file |
diff |
annotate
|
| Thu, 16 Jan 1997 14:53:37 +0100 |
wenzelm |
added termless parameter;
|
file |
diff |
annotate
|
| Fri, 10 Jan 1997 10:27:57 +0100 |
wenzelm |
cleaned up (real changes next time);
|
file |
diff |
annotate
|
| Wed, 29 May 1996 12:03:32 +0200 |
nipkow |
Added addsolver
|
file |
diff |
annotate
|
| Tue, 23 Apr 1996 17:11:23 +0200 |
oheimb |
*** empty log message ***
|
file |
diff |
annotate
|
| Fri, 16 Feb 1996 18:00:47 +0100 |
paulson |
Elimination of fully-functorial style.
|
file |
diff |
annotate
|
| Wed, 04 Oct 1995 12:53:35 +0100 |
clasohm |
renamed SS to Simpset; fixed bug in merge_ss
|
file |
diff |
annotate
|
| Fri, 01 Sep 1995 13:32:13 +0200 |
clasohm |
added global simpset
|
file |
diff |
annotate
|
| Thu, 30 Mar 1995 13:48:30 +0200 |
lcp |
Precedence of infixes is now 4 (just above that of :=)
|
file |
diff |
annotate
|
| Tue, 21 Jun 1994 11:55:36 +0200 |
nipkow |
improved error msg
|
file |
diff |
annotate
|
| Tue, 31 May 1994 13:17:41 +0200 |
nipkow |
simpset is hidden in a functor now.
|
file |
diff |
annotate
|
| Wed, 05 Jan 1994 19:47:14 +0100 |
nipkow |
got rid of METAHYPS due to the change of the basic simplification routines
|
file |
diff |
annotate
|
| Thu, 25 Nov 1993 13:41:08 +0100 |
nipkow |
asm_full_simp_tac now fails if there are no subgoals
|
file |
diff |
annotate
|
| Fri, 29 Oct 1993 11:54:50 +0100 |
nipkow |
added infix delsimps
|
file |
diff |
annotate
|
| Fri, 01 Oct 1993 13:26:22 +0100 |
nipkow |
asm_full_simp_tac now fails when applied to a state w/o subgoals.
|
file |
diff |
annotate
|
| Thu, 16 Sep 1993 14:21:44 +0200 |
nipkow |
changed addcongs to addeqcongs in simplifier.ML
|
file |
diff |
annotate
|
| Thu, 16 Sep 1993 12:20:38 +0200 |
clasohm |
Initial revision
|
file |
diff |
annotate
|