| Sat, 30 Dec 2006 16:08:00 +0100 |
wenzelm |
removed conditional combinator;
|
file |
diff |
annotate
|
| Thu, 07 Dec 2006 23:16:55 +0100 |
wenzelm |
reorganized structure Tactic vs. MetaSimplifier;
|
file |
diff |
annotate
|
| Tue, 05 Dec 2006 00:30:38 +0100 |
wenzelm |
thm/prf: separate official name vs. additional tags;
|
file |
diff |
annotate
|
| Thu, 30 Nov 2006 14:17:29 +0100 |
wenzelm |
qualified MetaSimplifier.norm_hhf(_protect);
|
file |
diff |
annotate
|
| Wed, 29 Nov 2006 04:11:09 +0100 |
wenzelm |
simplified Logic.count_prems;
|
file |
diff |
annotate
|
| Tue, 28 Nov 2006 00:35:18 +0100 |
wenzelm |
simplified '?' operator;
|
file |
diff |
annotate
|
| Fri, 24 Nov 2006 22:05:12 +0100 |
wenzelm |
ProofContext.init;
|
file |
diff |
annotate
|
| Fri, 10 Nov 2006 07:44:47 +0100 |
haftmann |
introduces canonical AList functions for loop_tacs
|
file |
diff |
annotate
|
| Wed, 11 Oct 2006 10:49:36 +0200 |
haftmann |
abandoned findrep
|
file |
diff |
annotate
|
| Mon, 09 Oct 2006 02:19:57 +0200 |
wenzelm |
Drule.lhs/rhs_of;
|
file |
diff |
annotate
|
| Thu, 21 Sep 2006 19:05:08 +0200 |
wenzelm |
member (op =);
|
file |
diff |
annotate
|
| Mon, 18 Sep 2006 19:39:07 +0200 |
wenzelm |
Thm.dest_arg;
|
file |
diff |
annotate
|
| Fri, 15 Sep 2006 20:08:38 +0200 |
wenzelm |
rrule: maintain 'extra' field for rule that contain extra vars outside elhs;
|
file |
diff |
annotate
|
| Thu, 03 Aug 2006 17:30:38 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 02 Aug 2006 22:26:41 +0200 |
wenzelm |
normalized Proof.context/method type aliases;
|
file |
diff |
annotate
|
| Sun, 30 Jul 2006 21:28:52 +0200 |
wenzelm |
Thm.adjust_maxidx;
|
file |
diff |
annotate
|
| Thu, 27 Jul 2006 13:43:06 +0200 |
wenzelm |
moved Goal.norm_hhf(_protect) to meta_simplifier.ML (pervasive);
|
file |
diff |
annotate
|
| Tue, 25 Jul 2006 21:18:04 +0200 |
wenzelm |
use Term.add_vars instead of obsolete term_varnames;
|
file |
diff |
annotate
|
| Tue, 18 Jul 2006 20:01:41 +0200 |
wenzelm |
Term.declare_term_names;
|
file |
diff |
annotate
|
| Tue, 11 Jul 2006 12:17:04 +0200 |
wenzelm |
replaced Term.variant(list) by Name.variant(_list);
|
file |
diff |
annotate
|
| Sat, 08 Jul 2006 12:54:45 +0200 |
wenzelm |
tuned exception handling;
|
file |
diff |
annotate
|
| Thu, 06 Jul 2006 16:49:40 +0200 |
wenzelm |
add/del_simps: warning for inactive simpset (no context);
|
file |
diff |
annotate
|
| 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
|