| Sun, 22 May 2005 16:51:07 +0200 |
wenzelm |
Simplifier already setup in Pure;
|
file |
diff |
annotate
|
| Thu, 08 Jul 2004 19:34:56 +0200 |
wenzelm |
adapted type of simprocs;
|
file |
diff |
annotate
|
| Wed, 30 Apr 2003 18:30:57 +0200 |
ballarin |
Simplifier: congruence rule update.
|
file |
diff |
annotate
|
| Mon, 04 Nov 2002 14:17:00 +0100 |
berghofe |
Removed obsolete section about reordering assumptions.
|
file |
diff |
annotate
|
| Tue, 01 Oct 2002 14:44:43 +0200 |
berghofe |
Adapted to new simplifier.
|
file |
diff |
annotate
|
| Wed, 07 Aug 2002 20:11:07 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 07 Aug 2002 20:03:17 +0200 |
wenzelm |
Simplifier.simproc(_i);
|
file |
diff |
annotate
|
| Sat, 12 Jan 2002 16:37:58 +0100 |
wenzelm |
renamed forall_elim_vars_safe to gen_all;
|
file |
diff |
annotate
|
| Fri, 11 Jan 2002 14:44:24 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 23 Feb 2001 16:31:21 +0100 |
oheimb |
renamed addaltern to addafter, addSaltern to addSafter
|
file |
diff |
annotate
|
| Tue, 20 Feb 2001 18:47:06 +0100 |
oheimb |
debugging: replaced gen_all by forall_elim_vars_safe
|
file |
diff |
annotate
|
| Tue, 29 Aug 2000 00:54:22 +0200 |
wenzelm |
updated cong stuff;
|
file |
diff |
annotate
|
| Mon, 28 Aug 2000 13:52:38 +0200 |
wenzelm |
proper setup of iman.sty/extra.sty/ttbox.sty;
|
file |
diff |
annotate
|
| Tue, 25 Jul 2000 18:43:52 +0200 |
berghofe |
Corrected example which still used old primrec syntax.
|
file |
diff |
annotate
|
| Fri, 21 Jul 2000 17:41:59 +0200 |
oheimb |
removed safe_asm_full_simp_tac, added generic_simp_tac
|
file |
diff |
annotate
|
| Tue, 18 Jan 2000 11:33:31 +0100 |
paulson |
fixed many bad line & page breaks
|
file |
diff |
annotate
|
| Sun, 31 Oct 1999 20:11:23 +0100 |
wenzelm |
updated;
Isabelle99
|
file |
diff |
annotate
|
| Fri, 22 Oct 1999 20:24:13 +0200 |
wenzelm |
new flag debug_simp
|
file |
diff |
annotate
|
| Tue, 28 Sep 1999 14:15:57 +0200 |
nipkow |
documented type solver
|
file |
diff |
annotate
|
| Mon, 03 May 1999 19:03:35 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 29 Oct 1998 15:05:42 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 25 Sep 1998 15:54:29 +0200 |
oheimb |
improved indentation
|
file |
diff |
annotate
|
| Fri, 25 Sep 1998 15:21:07 +0200 |
wenzelm |
rearranged SIMPSET(');
|
file |
diff |
annotate
|
| Thu, 24 Sep 1998 16:53:00 +0200 |
oheimb |
improved description of looper and splitter
|
file |
diff |
annotate
|
| Mon, 24 Aug 1998 19:11:13 +0200 |
wenzelm |
emacs local vars;
|
file |
diff |
annotate
|
| Tue, 28 Jul 1998 16:33:43 +0200 |
paulson |
Changed "goal" to "Goal"
|
file |
diff |
annotate
|
| Wed, 20 May 1998 15:20:28 +0200 |
nipkow |
Small mods.
|
file |
diff |
annotate
|
| Mon, 04 May 1998 09:17:18 +0200 |
nipkow |
New behaviour of asm_full_simp_tac.
|
file |
diff |
annotate
|
| Sat, 04 Apr 1998 14:30:19 +0200 |
wenzelm |
no open Simplifier;
|
file |
diff |
annotate
|
| Fri, 27 Feb 1998 11:18:16 +0100 |
oheimb |
added minimal description of rep_ss
|
file |
diff |
annotate
|
| Thu, 05 Feb 1998 10:26:59 +0100 |
paulson |
Fixed a lot of overfull and underfull lines (hboxes)
|
file |
diff |
annotate
|
| Mon, 12 Jan 1998 17:48:55 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 12 Jan 1998 17:26:00 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 12 Dec 1997 17:11:05 +0100 |
wenzelm |
major update;
|
file |
diff |
annotate
|
| Thu, 27 Nov 1997 19:39:02 +0100 |
wenzelm |
several minor updates;
|
file |
diff |
annotate
|
| Thu, 20 Nov 1997 11:54:31 +0100 |
paulson |
Updated the NatSum example
|
file |
diff |
annotate
|
| Mon, 20 Oct 1997 11:53:42 +0200 |
nipkow |
\label{simp-chap} -> chap:simplification
|
file |
diff |
annotate
|
| Wed, 02 Jul 1997 16:46:36 +0200 |
paulson |
Now there are TWO spaces after each full stop, so that the Emacs sentence
|
file |
diff |
annotate
|
| Wed, 07 May 1997 17:21:04 +0200 |
wenzelm |
fixed braces;
|
file |
diff |
annotate
|
| Wed, 07 May 1997 16:29:06 +0200 |
paulson |
New acknowledgements; fixed overfull lines and tables
|
file |
diff |
annotate
|
| Tue, 06 May 1997 13:42:28 +0200 |
wenzelm |
fixed simplifier examples;
|
file |
diff |
annotate
|
| Tue, 06 May 1997 12:50:16 +0200 |
wenzelm |
misc updates, tuning, cleanup;
|
file |
diff |
annotate
|
| Wed, 30 Apr 1997 16:33:43 +0200 |
paulson |
Indexing for trace_simp
|
file |
diff |
annotate
|
| Sat, 15 Feb 1997 17:35:53 +0100 |
oheimb |
corrected minor mistakes
|
file |
diff |
annotate
|
| Sat, 15 Feb 1997 16:10:00 +0100 |
oheimb |
description of del(eq)congs, safe and unsafe solver
|
file |
diff |
annotate
|
| Fri, 14 Feb 1997 10:35:42 +0100 |
paulson |
Updated documentation of IFOL_ss
|
file |
diff |
annotate
|
| Fri, 31 Jan 1997 15:54:00 +0100 |
oheimb |
added addloop (and also documentation of addsolver
|
file |
diff |
annotate
|
| Tue, 07 Jan 1997 10:17:07 +0100 |
paulson |
Updated account of implicit simpsets and clasets
|
file |
diff |
annotate
|
| Tue, 24 Sep 1996 13:51:10 +0200 |
paulson |
Restoration of reference to Nipkow, LICS, 1993
|
file |
diff |
annotate
|
| Mon, 15 Jul 1996 12:36:56 +0200 |
nipkow |
Documented simplification tactics which make use of the implicit simpset.
|
file |
diff |
annotate
|
| Thu, 07 Dec 1995 14:24:32 +0100 |
clasohm |
removed quotes from syntax and consts sections
|
file |
diff |
annotate
|
| Fri, 28 Jul 1995 19:17:03 +0200 |
nipkow |
added section on "Reordering assumptions".
|
file |
diff |
annotate
|
| Wed, 03 May 1995 16:30:39 +0200 |
lcp |
trivial rewording
|
file |
diff |
annotate
|
| Fri, 18 Nov 1994 13:04:51 +0100 |
nipkow |
Updated description of valid lhss.
|
file |
diff |
annotate
|
| Wed, 09 Nov 1994 15:47:11 +0100 |
lcp |
updated discussion of congruence rules in first section
|
file |
diff |
annotate
|
| Fri, 22 Apr 1994 18:18:37 +0200 |
lcp |
final Springer copy
|
file |
diff |
annotate
|
| Fri, 15 Apr 1994 17:16:23 +0200 |
lcp |
penultimate Springer draft
|
file |
diff |
annotate
|
| Mon, 21 Mar 1994 11:02:57 +0100 |
lcp |
first draft of Springer book
|
file |
diff |
annotate
|
| Fri, 19 Nov 1993 12:54:16 +0100 |
lcp |
Reformatting of SIMPLIFIER figure
|
file |
diff |
annotate
|
| Tue, 16 Nov 1993 14:13:11 +0100 |
clasohm |
replaced \un by \union in "Simplification sets"
|
file |
diff |
annotate
|