| Tue, 06 Jun 2006 20:42:28 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 11 May 2006 19:19:33 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 29 Apr 2006 23:16:43 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 27 Apr 2006 15:06:35 +0200 |
wenzelm |
tuned basic list operators (flat, maps, map_filter);
|
file |
diff |
annotate
|
| Tue, 21 Mar 2006 12:18:11 +0100 |
wenzelm |
gen_eq_set, remove (op =);
|
file |
diff |
annotate
|
| Sun, 26 Feb 2006 23:01:48 +0100 |
wenzelm |
rewrite_goals_rule_aux: actually use prems if present;
|
file |
diff |
annotate
|
| Wed, 15 Feb 2006 21:35:02 +0100 |
wenzelm |
rewrite_cterm: Thm.adjust_maxidx prevents unnecessary increments on rules;
|
file |
diff |
annotate
|
| Mon, 06 Feb 2006 20:58:54 +0100 |
wenzelm |
Envir.(beta_)eta_contract;
|
file |
diff |
annotate
|
| Wed, 04 Jan 2006 16:38:40 +0100 |
nipkow |
trace_simp_depth_limit is 1 by default
|
file |
diff |
annotate
|
| Thu, 22 Dec 2005 00:29:00 +0100 |
wenzelm |
renamed imp_cong' to imp_cong_rule;
|
file |
diff |
annotate
|
| Sat, 19 Nov 2005 14:21:05 +0100 |
wenzelm |
simpset: added reorient field, set_reorient;
|
file |
diff |
annotate
|
| Fri, 21 Oct 2005 18:14:46 +0200 |
wenzelm |
moved various simplification tactics and rules to simplifier.ML;
|
file |
diff |
annotate
|
| Tue, 18 Oct 2005 17:59:30 +0200 |
wenzelm |
renamed set_context to context;
|
file |
diff |
annotate
|
| Mon, 17 Oct 2005 23:10:20 +0200 |
wenzelm |
added set/addloop' for simpset dependent loopers;
|
file |
diff |
annotate
|
| Tue, 04 Oct 2005 19:01:37 +0200 |
wenzelm |
minor tweaks for Poplog/ML;
|
file |
diff |
annotate
|
| Thu, 29 Sep 2005 15:50:46 +0200 |
wenzelm |
export debug_bounds;
|
file |
diff |
annotate
|
| Thu, 29 Sep 2005 12:33:26 +0200 |
berghofe |
Simplifier now removes flex-flex constraints from theorem returned by prover.
|
file |
diff |
annotate
|
| Thu, 29 Sep 2005 00:58:58 +0200 |
wenzelm |
removed revert_bound;
|
file |
diff |
annotate
|
| Fri, 23 Sep 2005 22:21:54 +0200 |
wenzelm |
added mk_solver';
|
file |
diff |
annotate
|
| Tue, 20 Sep 2005 08:21:49 +0200 |
haftmann |
slight adaptions to library changes
|
file |
diff |
annotate
|
| Fri, 02 Sep 2005 15:54:47 +0200 |
haftmann |
some 'assoc' etc. refactoring
|
file |
diff |
annotate
|
| Wed, 31 Aug 2005 15:46:40 +0200 |
wenzelm |
refer to theory instead of low-level tsig;
|
file |
diff |
annotate
|
| Tue, 16 Aug 2005 12:51:07 +0200 |
nipkow |
simp_depth warning now mod 20, not mod 10 (too often)
|
file |
diff |
annotate
|
| Mon, 01 Aug 2005 19:20:39 +0200 |
wenzelm |
improved bounds: nameless Term.bound, recover names for output;
|
file |
diff |
annotate
|
| Thu, 28 Jul 2005 15:19:55 +0200 |
wenzelm |
Term.bound;
|
file |
diff |
annotate
|
| Fri, 15 Jul 2005 15:44:15 +0200 |
wenzelm |
tuned fold on terms;
|
file |
diff |
annotate
|
| Thu, 14 Jul 2005 19:28:24 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 13 Jul 2005 16:07:28 +0200 |
wenzelm |
export eq_rrule;
|
file |
diff |
annotate
|
| Fri, 01 Jul 2005 22:33:59 +0200 |
wenzelm |
decomp_simp: compare terms, not cterms;
|
file |
diff |
annotate
|
| Fri, 17 Jun 2005 18:35:27 +0200 |
wenzelm |
accomodate change of TheoryDataFun;
|
file |
diff |
annotate
|