| Mon, 13 Jun 2005 13:10:45 +0200 |
nipkow |
changed -1 back to 0
|
file |
diff |
annotate
|
| Sun, 12 Jun 2005 08:53:41 +0200 |
nipkow |
simp_depth now starts at -1 to make it start at 0 ;-)
|
file |
diff |
annotate
|
| Mon, 06 Jun 2005 19:09:49 +0200 |
nipkow |
Added the t = x "fix" - in (* ... *) :-(
|
file |
diff |
annotate
|
| Mon, 23 May 2005 11:14:58 +0200 |
nipkow |
tuned trace info (depth)
|
file |
diff |
annotate
|
| Fri, 04 Mar 2005 15:07:34 +0100 |
skalberg |
Removed practically all references to Library.foldr.
|
file |
diff |
annotate
|
| Thu, 03 Mar 2005 12:43:01 +0100 |
skalberg |
Move towards standard functions.
|
file |
diff |
annotate
|
| Sun, 13 Feb 2005 17:15:14 +0100 |
skalberg |
Deleted Library.option type.
|
file |
diff |
annotate
|
| Mon, 24 Jan 2005 18:11:06 +0100 |
berghofe |
Removed unnecessary subsignature checks to speed up rewriting.
|
file |
diff |
annotate
|
| Mon, 18 Oct 2004 11:43:40 +0200 |
berghofe |
Replaced list of bound variables in simpset by maximal index of bound
|
file |
diff |
annotate
|
| Sat, 11 Sep 2004 18:35:43 +0200 |
nipkow |
undoing previous change
|
file |
diff |
annotate
|
| Fri, 10 Sep 2004 00:19:15 +0200 |
nipkow |
new forward deduction capability for simplifier
|
file |
diff |
annotate
|
| Fri, 30 Jul 2004 10:41:52 +0200 |
wenzelm |
tuned output;
|
file |
diff |
annotate
|
| Sun, 11 Jul 2004 20:34:50 +0200 |
wenzelm |
improved print_ss; tuned;
|
file |
diff |
annotate
|
| Thu, 08 Jul 2004 19:33:51 +0200 |
wenzelm |
major cleanup; got rid of obsolete meta_simpset;
|
file |
diff |
annotate
|
| Wed, 30 Jun 2004 00:42:59 +0200 |
skalberg |
Made simplification procedures simpset-aware.
|
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
|
| Wed, 23 Jun 2004 14:44:22 +0200 |
skalberg |
Moved conversion rules from MetaSimplifier to Drule. refl_implies removed
|
file |
diff |
annotate
|
| Mon, 21 Jun 2004 10:25:57 +0200 |
kleing |
Merged in license change from Isabelle2004
|
file |
diff |
annotate
|
| Thu, 22 Apr 2004 10:52:32 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 25 Dec 2003 23:18:04 +0100 |
nipkow |
Added trace msg
|
file |
diff |
annotate
|
| Tue, 21 Oct 2003 11:09:23 +0200 |
skalberg |
Added access to the mk_rews field (and friends).
|
file |
diff |
annotate
|
| Tue, 20 May 2003 11:52:42 +0200 |
kleing |
be less verbose about simplification depth
|
file |
diff |
annotate
|
| Mon, 28 Apr 2003 12:01:45 +0200 |
ballarin |
Simplifier no longer aborts on failed congruence proof.
|
file |
diff |
annotate
|
| Thu, 27 Feb 2003 15:12:29 +0100 |
ballarin |
Change to meta simplifier: congruence rules may now have frees as head of term.
|
file |
diff |
annotate
|
| Tue, 25 Feb 2003 18:49:23 +0100 |
nipkow |
added simp_depth_limit
|
file |
diff |
annotate
|
| Mon, 21 Oct 2002 17:09:31 +0200 |
berghofe |
No more explicit manipulation of flex-flex constraints in goals_conv.
|
file |
diff |
annotate
|
| Tue, 01 Oct 2002 11:17:25 +0200 |
berghofe |
Deleted superfluous dest_implies.
|
file |
diff |
annotate
|
| Mon, 30 Sep 2002 16:38:22 +0200 |
berghofe |
Completely reimplemented mutual simplification of premises.
|
file |
diff |
annotate
|
| Thu, 19 Sep 2002 16:01:29 +0200 |
nipkow |
drule: added nRS
|
file |
diff |
annotate
|
| Thu, 08 Aug 2002 23:51:24 +0200 |
wenzelm |
exception SIMPROC_FAIL: solid error reporting of simprocs;
|
file |
diff |
annotate
|