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
|