| Thu, 28 Feb 2002 19:22:56 +0100 |
wenzelm |
decomp_simp': use lhs instead of elhs (preserves more bound variable names);
|
file |
diff |
annotate
|
| Wed, 16 Jan 2002 23:17:44 +0100 |
wenzelm |
interface to Pattern.rewrite_term;
|
file |
diff |
annotate
|
| Wed, 16 Jan 2002 20:58:27 +0100 |
wenzelm |
export beta_eta_conversion;
|
file |
diff |
annotate
|
| Thu, 27 Dec 2001 16:46:52 +0100 |
wenzelm |
tuned tracing markup;
|
file |
diff |
annotate
|
| Sat, 24 Nov 2001 16:56:26 +0100 |
wenzelm |
gen_merge_lists;
|
file |
diff |
annotate
|
| Wed, 21 Nov 2001 00:36:51 +0100 |
wenzelm |
use tracing function for trace output;
|
file |
diff |
annotate
|
| Mon, 12 Nov 2001 10:44:55 +0100 |
berghofe |
congc now returns None if congruence rule has no effect.
|
file |
diff |
annotate
|
| Mon, 22 Oct 2001 18:01:38 +0200 |
wenzelm |
Display.pretty_thms;
|
file |
diff |
annotate
|
| Sun, 14 Oct 2001 22:05:01 +0200 |
wenzelm |
tuned rewrite/simplify interface;
|
file |
diff |
annotate
|
| Sun, 14 Oct 2001 20:08:11 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 12 Oct 2001 18:29:51 +0200 |
berghofe |
Tuned comment.
|
file |
diff |
annotate
|
| Fri, 12 Oct 2001 16:57:07 +0200 |
berghofe |
- Exported goals_conv and fconv_rule
|
file |
diff |
annotate
|
| Thu, 04 Oct 2001 16:07:20 +0200 |
wenzelm |
removed obsolete comment;
|
file |
diff |
annotate
|
| Thu, 04 Oct 2001 15:21:47 +0200 |
wenzelm |
full_rewrite_cterm_aux (see also tactic.ML);
|
file |
diff |
annotate
|
| Tue, 28 Aug 2001 14:25:26 +0200 |
nipkow |
Implemented indentation schema for conditional rewrite trace.
|
file |
diff |
annotate
|
| Thu, 23 Aug 2001 14:32:48 +0200 |
nipkow |
Traced depth of conditional rewriting
|
file |
diff |
annotate
|
| Mon, 11 Jun 2001 19:21:13 +0200 |
berghofe |
Fixed bug in function rebuild.
|
file |
diff |
annotate
|
| Thu, 10 May 2001 17:28:40 +0200 |
nipkow |
improved tracing of permutative rules.
|
file |
diff |
annotate
|
| Wed, 09 May 2001 23:09:26 +0200 |
nipkow |
improved simproc trace IGNORED
|
file |
diff |
annotate
|
| Wed, 03 Jan 2001 21:18:31 +0100 |
wenzelm |
Thm: dest_comb, dest_abs, capply, cabs no longer global;
|
file |
diff |
annotate
|
| Tue, 07 Nov 2000 17:44:48 +0100 |
berghofe |
Added new file meta_simplifier.ML
|
file |
diff |
annotate
|